Hanoi tower in Coq
| File | Content |
|---|---|
| extra | Extra theorems from the standard library |
| gdist | Distance in a graph |
| ghanoi | General Hanoi framework |
| ghanoi3 | General Hanoi framework with 3 pegs |
| lhanoi3 | Linear Hanoi tower with 3 pegs |
| rhanoi3 | Regular Hanoi tower with 3 pegs |
| triangular | Theorems about triangular numbers |
| phi | Theorems about the Φ function |
| psi | Theorems about the Ψ function |
| ghanoi4 | General Hanoi framework with 4 pegs |
| rhanoi4 | Regular Hanoi tower with 4 pegs |
| star | Some maths for the shanoi |
| shanoi | Hanoi tower in star |
| shanoi4 | Hanoi tower with 4 pegs in star |
A note about this development is available here.
An interactive version of the library is available here.
To build the library, download the files and type opam install . or manually type make and then make install (the dependencies are listed in opam).