hanoi

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.

Meta

• Author(s):
  • Laurent Théry
• License: MIT License
• Compatible Coq versions: 8.18 or later
• Additional dependencies:
  • MathComp ssreflect 2.1 or later
  • MathComp algebra 2.1 or later
  • MathComp finmap 2.0 or later
  • MathComp bigenough 1.0.1 or later
• Coq namespace: hanoi
• Related publication(s): none

Building and installation instructions

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