automata 6 | |
automata 5 | |
automata 4 | |
myhill nerode | |
det automata | |
action sets | |
languages | |
relation autom | |
quot 1 | Support lemmas for quotient type. |
exponent | |
list 3 autom | |
finite sets | |
list 1 | |
int 2 | Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles. |
choice 1 | |
rel 1 | Common properties of binary relations. |
bool 1 | Definitions, theorems and tactics for the boolean type and boolean-related expressions. |
int 1 | Integer inequalities, subtypes, and induction lemmas for subtypes. |
well fnd | Well-founded predicate. Rank induction lemmas and tactics. |
fun 1 | Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity. |
core | Some basic concepts defined type-theoretically. |