Data.Binding.Hobbits.Internal

This module is internal to the Hobbits library, and should not be used directly.

Documentation

newtype Name a

A Name a is a bound name that is associated with type a.

Constructors

MkName Int

Instances

Typeable1 Name

Eq (Name a)

Show (Name a)

NuElim (Name a)

Show (MapC Name c)

data Mb ctx b

An Mb ctx b is a multi-binding that binds exactly one name for each type in ctx, where ctx has the form Nil :> t1 :> ... :> tn.

Constructors

MkMb (MapC Name ctx) b

Instances

Typeable2 Mb

Show a => Show (Mb c a)

NuElim a => NuElim (Mb ctx a)

newtype Cl a

The type Cl a represents a closed term of type a, i.e., an expression of type a with no free (Haskell) variables. Since this cannot be checked directly in the Haskell type system, the Cl data type is hidden, and the user can only create closed terms using Template Haskell, through the mkClosed operator.

Constructors

Cl

Fields

unCl :: a

data ExMember where

Constructors

ExMember :: Member c a -> ExMember

memberFromLen :: Int -> ExMember

unsafeLookupC :: Int -> Member c a

data ExProxy where

Constructors

ExProxy :: MapC Proxy ctx -> ExProxy

proxyFromLen :: Int -> ExProxy

unsafeProxyFromLen :: Int -> MapC Proxy ctx

unsafeNamesFromInts :: [Int] -> MapC Name ctx

counter :: IORef Int

fresh_name :: a -> Int

fresh_names :: MapC Name ctx -> MapC Name ctx