Skip to content

Instantly share code, notes, and snippets.

@marcosh
Created October 6, 2017 09:56
Show Gist options
  • Save marcosh/d51479ea08e8522560713fd1e5ca9624 to your computer and use it in GitHub Desktop.
Save marcosh/d51479ea08e8522560713fd1e5ca9624 to your computer and use it in GitHub Desktop.
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
Copy link

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