Project Page
Index
Table of Contents
Ltac2Tutorial.tutorial0
Ltac2 Tutorial: Programming basics and proof state manipulation
Proof mode and namespace
Arithmetic expressions
Algebraic data types
Record types
Constructing Gallina terms
Manipulating proof state
Our first tactic
Extra: More on constr
Bonus: Traverse the Gallina AST explicitly
Ltac2Tutorial.tutorial1
Ltac2Tutorial.tutorial2