Library tactics
Library base
- Generic lemmas not in Ssreflect
- Alternative membership for {set seq_sub xs}
- Trees
- A least fixed point operator for finType
- Decidability
- Some lemmas, that allow classical reasoning in some circumstances
Library P
Library Kstar
- Models
- Generic construction of finite models
- Syntax
- Evaluation
- Formula Universe
- Hintikka sets, Hintikka systems and demos
- Pruning
Library Hstar
- Models
- Generic construction of finite models
- Syntax
- Evaluation
- Formula Universe
- Nominals
- Hintikka sets, Hintikka systems and demos
- Pruning
Library Kstar_strong
Library UB
This page has been generated by coqdoc