[−][src]Module dependent_ghost::proof
Structs
And | Conjunction. |
Equiv | Equivalence. This could be defined in terms of |
FALSE | The trivial false proposition. |
Implies | Implication. |
Neg | Negation. |
Or | Disjunction. |
Proof | A value of type |
SuchThat | A value of type |
TRUE | Proposition constructors |
Functions
absurd | |
and_elim_l | |
and_elim_r | |
and_intro | Proof combinators |
axiom | Define an axiom that is trivially true in an underlying theory. This will be most useful in defining domain-specific laws about the behavior of some data structure described by a ghostly type. For example, we might encode the fact that adding a key to a map leaves the other keys untouched as an axiom. |
contradict | |
equiv_elim | |
equiv_intro | |
false_elim | |
impl_elim | |
impl_intro | |
modus_ponens | |
neg_elim | |
neg_intro | |
or_intro_l | |
or_intro_r | |
refl | The following functions are aliases for the above combinators. Use them if you think it makes your logic clearer. |
such_that | Annotate a value with a proof. |
true_intro |