Skip to content

Instantly share code, notes, and snippets.

@puffnfresh

puffnfresh/bowling.idr

Last active August 29, 2015 14:12
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save puffnfresh/3739b6bd857c0e5459e2 to your computer and use it in GitHub Desktop.
Save puffnfresh/3739b6bd857c0e5459e2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
bowling.idr
data First : Nat -> Type where
MkFirst : (n : Fin 10) -> First (finToNat n)
data Second : Nat -> Type where
MkSecond : (f : First m) -> (n : Fin m) -> Second (finToNat n)
MkNoSecond : (f : First 9) -> Second 0
hit8 : Second 1
hit8 = MkSecond (MkFirst 8) (FS FZ)
strike : Second 0
strike = MkNoSecond (MkFirst 9)
@ToJans
Copy link

ToJans commented Dec 29, 2014

Awesome; thank you!

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