hobbits-1.2.1: 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
LanguageHaskell98

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 

Instances

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 

Instances

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) 

Instances

data Decls :: * -> * where Source

Constructors

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

Instances