Hanoi.idr

data Selection : Type where
  Empty : Selection
  InHand : Nat -> Selection

Tower : Type
Tower = List Nat

data Hanoi : Selection -> Tower -> Tower -> Tower -> Type where
  Start : Hanoi Empty [1,2,3,4,5] [] []
  Take1 : Hanoi Empty (x::xs) ys zs -> Hanoi (InHand x) xs ys zs
  Take2 : Hanoi Empty xs (y::ys) zs -> Hanoi (InHand y) xs ys zs
  Take3 : Hanoi Empty xs ys (z::zs) -> Hanoi (InHand z) xs ys zs
  Put1 : Hanoi (InHand w) [] ys zs -> Hanoi Empty [w] ys zs
  Put2 : Hanoi (InHand w) xs [] zs -> Hanoi Empty xs [w] zs
  Put3 : Hanoi (InHand w) xs ys [] -> Hanoi Empty xs ys [w]
  Stack1 : LT w x -> Hanoi (InHand w) (x::xs) ys zs -> Hanoi Empty (w::x::xs) ys zs
  Stack2 : LT w y -> Hanoi (InHand w) xs (y::ys) zs -> Hanoi Empty xs (w::y::ys) zs
  Stack3 : LT w z -> Hanoi (InHand w) xs ys (z::zs) -> Hanoi Empty xs ys (w::z::zs)

solve : Hanoi Empty [] [] [1,2,3,4,5]
solve = ?hmm

badState : Hanoi (InHand 1) [1,2,3,4,5] [] [] -> Void
badState = ?goodLuck