bool_compset

computeLib.bool_compset : compset

A simplification set for use with CBV_CONV for basic computations.

This compset is a simplification set for use with the compute library performing computations about operations on primitive booleans and other basic constants, such as LET, conditional, implication, conjunction, disjunction, and negation.

Example

> computeLib.CBV_CONV computeLib.bool_compset (Term `F ==> (T \/ F)`);
val it = ⊢ F ⇒ T ∨ F ⇔ T: thm

See also

computeLib.CBV_CONV