Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Documentation

data L a

data D a

data Term :: * -> * where

Constructors

Var :: Name (L a) -> Term a

Lam :: Binding (L b) (Term a) -> Term (b -> a)

App :: Term (b -> a) -> Term b -> Term a

Instances

Show (Term a)

NuMatching (Term a)

lam :: (Term a -> Term b) -> Term (a -> b)

data DTerm :: * -> * where

Constructors

TVar :: Name (L a) -> DTerm a

TDVar :: Name (D a) -> DTerm a

TApp :: DTerm (a -> b) -> DTerm a -> DTerm b

Instances

Show (DTerm a)

NuMatching (DTerm a)

data Decl :: * -> * where

Constructors

Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)

Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)

Instances

NuMatching (Decl a)

data Decls :: * -> * where

Constructors

Decls_Base :: DTerm a -> Decls a

Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a

Instances

Show (Decls a)

NuMatching (Decls a)