Skip to main content

Module equiv

logicaffeine_tv

Module equiv 

Source
Expand description

The SMT equivalence primitive, built on logicaffeine_verify::check_equivalence.

Functionsยง

is_valid
True iff prove_valid proves the predicate.
prove_valid
Prove that a Bool-sorted VerifyExpr is valid (true under every assignment of its free variables).