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 
Instances
Show (Term a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

showsPrec :: Int -> Term a -> ShowS #

show :: Term a -> String #

showList :: [Term a] -> ShowS #

NuMatching (Term a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

nuMatchingProof :: MbTypeRepr (Term a) Source #

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
Show (DTerm a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

showsPrec :: Int -> DTerm a -> ShowS #

show :: DTerm a -> String #

showList :: [DTerm a] -> ShowS #

NuMatching (DTerm a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

nuMatchingProof :: MbTypeRepr (DTerm a) Source #

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
NuMatching (Decl a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

nuMatchingProof :: MbTypeRepr (Decl a) Source #

data Decls :: * -> * where Source #

Constructors

Decls_Base :: DTerm a -> Decls a 
Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a 
Instances
Show (Decls a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

showsPrec :: Int -> Decls a -> ShowS #

show :: Decls a -> String #

showList :: [Decls a] -> ShowS #

NuMatching (Decls a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

Methods

nuMatchingProof :: MbTypeRepr (Decls a) Source #