Hanoi - 0.1.0

Hanoi

Description

Towers of Hanoi is a puzzle with three rods and n disks of decresing size. The disks are stacked ontop of each other through the first rod. The aim of the game is to move the stack of disks to another rod while following these rules: 1. Only one disk can be moved at a time 2. You may only move a disk from the top of one of the stacks to the top of another stack 3. No disk may be moved on top of a smaller disk The function hanoi computes the sequence of moves to solve puzzle.

Definitions

axiom ++str : String String StringSource#

Concatenation of Strings

concat : List String StringSource#

Concatenates a list of strings concat (("a" :: nil) :: "b" :: nil) evaluates to "a" :: "b" :: nil

unlines : List String StringSource#

Joins a list of strings with the newline character

singleton : {A : Type} A List ASource#

Produce a singleton List

showList : List Nat StringSource#

Produce a String representation of a List Nat

type PegSource#

A Peg represents a peg in the towers of Hanoi game

Constructors

left : Peg
middle : Peg
right : Peg

type MoveSource#

A Move represents a move between pegs

Constructors

move : Peg Peg Move

hanoi : Nat Peg Peg Peg List MoveSource#

Produce a list of Moves that solves the towers of Hanoi game