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.
- Author(s):
- Laurent Théry
- License: MIT License
- Compatible Coq versions: 8.18 or later
- Additional dependencies:
- Coq namespace:
hanoi - Related publication(s): none
To build and install manually, do:
git clone https://github.com/thery/hanoi.git
cd hanoi
make # or make -j <number-of-cores-on-your-machine>
make install