Struct dependent_ghost::proof::TRUE

pub struct TRUE;

Proposition constructors

The following logical combinators exist to encode a basic propositional logic (specifically, the rules of intuitionistic natural deduction) into Rust's typesystem. As usual, all of these types are zero-sized and will have no runtime impact.

With these combinators, users can construct their own proofs of properties that a library author may want to ensure (such as ensuring that a list is non-empty, a key exists in a map, and so on). The trivial true proposition.