Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Safe Haskell | Safe-Infered |
This module is internal to the Hobbits library, and should not be used directly.
- newtype Name a = MkName Int
- data Mb ctx b = MkMb (MapC Name ctx) b
- newtype Cl a = Cl {
- unCl :: a
- data ExMember where
- memberFromLen :: Int -> ExMember
- unsafeLookupC :: Int -> Member c a
- data ExProxy where
- proxyFromLen :: Int -> ExProxy
- unsafeProxyFromLen :: Int -> MapC Proxy ctx
- unsafeNamesFromInts :: [Int] -> MapC Name ctx
- counter :: IORef Int
- fresh_name :: a -> Int
Documentation
A Name a
is a bound name that is associated with type 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.
memberFromLen :: Int -> ExMemberSource
unsafeLookupC :: Int -> Member c aSource
proxyFromLen :: Int -> ExProxySource
unsafeProxyFromLen :: Int -> MapC Proxy ctxSource
unsafeNamesFromInts :: [Int] -> MapC Name ctxSource
fresh_name :: a -> IntSource