Skip to content

Instantly share code, notes, and snippets.

@bvssvni bvssvni/test.idr
Created Apr 4, 2017

What would you like to do?
Attempt to generate a function type
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
You can’t perform that action at this time.