hobbits-1.3: A library for canonically representing terms with binding

Copyright(c) 2011 Edwin Westbrook Nicolas Frisby and Paul Brauner
LicenseBSD3
Maintaineremw4@rice.edu
Stabilityexperimental
PortabilityGHC
Safe HaskellNone
LanguageHaskell2010

Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Description

 

Documentation

data L a Source #

data D a Source #

data Term :: * -> * where Source #

Constructors

Var :: Name (L a) -> Term a 
Lam :: Binding (L b) (Term a) -> Term (b -> a) 
App :: Term (b -> a) -> Term b -> Term a 

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

data DTerm :: * -> * where Source #

Constructors

TVar :: Name (L a) -> DTerm a 
TDVar :: Name (D a) -> DTerm a 
TApp :: DTerm (a -> b) -> DTerm a -> DTerm b 

data Decl :: * -> * where Source #

Constructors

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

data Decls :: * -> * where Source #

Constructors

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