| Module | Purpose |
|---|---|
| Term.lhs | Defines the type of propositional expressions (terms) |
| Theorem.lhs | Defines the type of theorems and primitive inference rules |
| Inferences.lhs | Examples of adding your own inference rules |
| InfLib.lhs | Some inference rules the next two modules need |
| Tactical.lhs | Goal-directed backward inferences, aka tactics |
| MonadicTactical | Goal-directed backward inferences are monads! |