Module prop

Re-exports

pub use constructors::eq;

Modules

constructors

This module provides monomorphic constructors for Prop. Hax rewrite more elaborated versions (see forall or AndBit below) to those monomorphic constructors.

Structs

Prop

Represent a logical proposition, that may be not computable.

Traits

ToProp

Functions

exists

The existential quantifier. This should be used only for Hax code: in Rust, this is always true.

forall

The universal quantifier. This should be used only for Hax code: in Rust, this is always true.

implies

The logical implication a ==> b.