Library libs.bcase
A simple checker for boolean tautologies
Library libs.edone
A slightly more powerful done tactic
Library libs.base
Generic Lemmas not in Ssreflect
A least- and greatest fixpoints for finite types
Cyclic directed distance
Library libs.fset
Finite Sets over choice types and countable types
Primitive operations
Notations
Basic Theory
Subset
Big Unions
Cardinality / Size
Weight function for sets
Fixpoints
Reachability withing a set
Maximal extensions
Pruning
Rudimentary Automation
Library libs.fset_tac
Automation for finite Sets
Tableau rules
Implementation of the Tactic
User-level Tactics
Library libs.induced_sym
Induced Symmetric Subrelations
Library libs.modular_hilbert
A Modular Library for Reasoing in Hilbert Systems
Minimal Logic
Propositional Logic
Basic Propositional Logic Facts
Equivalence (Experimental)
Big Boolean Operators
Remaining Propostional Logic Facts
Basic Modal Logic
K*
CTL
Library libs.sltype
Generic Lemmas for Literals and Support
This page has been generated by
coqdoc