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)

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 [Int] b

Instances

Typeable2 Mb

Show a => Show (Mb c a)

NuElim a => NuElim (Mb ctx 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