ATBR.Common
ATBR.BoolView
- bool_simpl is a tactic that simplifies boolean operations in the context and in the goal
- bool_connectors takes hypothesis like ((x && y) || negb z) = true and transforms them into
ATBR.MyFSets
ATBR.MyFSetProperties
ATBR.MyFMapProperties
ATBR.Numbers
- The NUM interface
- Notations, lemmas and tactics derivable from the NUM interface
- num_analyse : destroys the boolean expressions
- num_prop : transforms atoms like leb x y = true into le x y
- num_omega : injects every prop about nums into equivalent props about nats, then call omega
- Instance of NUM with positive as base type