| Copyright | (c) 2011 Edwin Westbrook Nicolas Frisby and Paul Brauner |
|---|---|
| License | BSD3 |
| Maintainer | emw4@rice.edu |
| Stability | experimental |
| Portability | GHC |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Binding.Hobbits.Examples.LambdaLifting.Terms
Description
Documentation
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 # | |
| NuMatching (Term a) Source # | |
Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms Methods nuMatchingProof :: MbTypeRepr (Term a) 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 # | |
| NuMatching (DTerm a) Source # | |
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 # | |
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 # | |
| NuMatching (Decls a) Source # | |
Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms Methods nuMatchingProof :: MbTypeRepr (Decls a) Source # | |