Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module Hanoi
import Data.Vect
data Peg
= First
| Second
| Third
-- TODO : can we do better here?
Eq Peg where
First == First = True
Second == Second = True
Third == Third = True
_ == _ = False
Disposition : Nat -> Type
Disposition diskNumber = Vect diskNumber Peg
startingDisposition : (diskNumber: Nat) -> Disposition diskNumber
startingDisposition diskNumber = replicate diskNumber First
data So : Bool -> Type where
Oh : So True
tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) =
map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)
@anton-trunov

This comment has been minimized.

Copy link

@anton-trunov anton-trunov commented Oct 6, 2017

You can import Data.So instead of defining your own version of it

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment