Skip to content

Instantly share code, notes, and snippets.

@bvssvni

bvssvni/test.idr

Created April 4, 2017 17:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bvssvni/776ad5d97b9ecdbe7a4b12fe362aecd8 to your computer and use it in GitHub Desktop.
Save bvssvni/776ad5d97b9ecdbe7a4b12fe362aecd8 to your computer and use it in GitHub Desktop.
Download ZIP
Attempt to generate a function type
Raw
test.idr
data PathType = NAT | BOOL
interpPathType : PathType -> Type
interpPathType NAT = Nat
interpPathType BOOL = Bool
Func : Type
Func = (List PathType, PathType)
interp : Func -> Type
interp ([], b) = interpPathType b
interp (a :: as, b) = (interpPathType a) -> (interp (as, b))
inc : Nat -> Nat
inc x = S x
foo : interp ([NAT], NAT) -> Nat
foo f = f 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment