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)

Methods

showsPrec :: Int -> Term a -> ShowS

show :: Term a -> String

showList :: [Term a] -> ShowS

NuMatching (Term a0)

Methods

nuMatchingProof :: MbTypeRepr (Term a0)

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)

Methods

showsPrec :: Int -> DTerm a -> ShowS

show :: DTerm a -> String

showList :: [DTerm a] -> ShowS

NuMatching (DTerm a0)

Methods

nuMatchingProof :: MbTypeRepr (DTerm a0)

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 a0)

Methods

nuMatchingProof :: MbTypeRepr (Decl a0)

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)

Methods

showsPrec :: Int -> Decls a -> ShowS

show :: Decls a -> String

showList :: [Decls a] -> ShowS

NuMatching (Decls a0)

Methods

nuMatchingProof :: MbTypeRepr (Decls a0)