Hanoi - 0.1.0

Hanoi

Description

Towers of Hanoi is a puzzle with three rods and n disks of decreasing size. The disks are stacked on top 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

concat (list : List String) : StringSource#

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

singleton {A} (a : A) : List ASource#

Produce a singleton List

showList (xs : 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
| middle
| right

type MoveSource#

A Move represents a move between pegs

Constructors

mkMove@{ from : Peg; to : Peg; }

hanoi : Nat -> Peg -> Peg -> Peg -> List MoveSource#

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