Module dependent_ghost::proof

Structs

And	Conjunction.
Equiv	Equivalence. This could be defined in terms of Implies, but is provided on its own for convenience.
FALSE	The trivial false proposition.
Implies	Implication.
Neg	Negation.
Or	Disjunction.
Proof	A value of type Proof<P> for some type-encoded property P is a proof of that property, which can be manipulated to form other proofs.
SuchThat	A value of type SuchThat<A,P> is a value of type A annotated with a proof of the proposition P.
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