| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Builtin
Synopsis
- bindBuiltin :: String -> ResolvedName -> TCM ()
- bindBuiltinNoDef :: String -> QName -> TCM ()
- builtinKindOfName :: String -> Maybe KindOfName
- bindPostulatedName :: String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
- isUntypedBuiltin :: String -> Bool
- bindUntypedBuiltin :: String -> ResolvedName -> TCM ()
Documentation
bindBuiltin :: String -> ResolvedName -> TCM () Source #
Bind a builtin thing to an expression.
bindBuiltinNoDef :: String -> QName -> TCM () Source #
Bind a builtin thing to a new name.
Since their type is closed, it does not matter whether we are in a parameterized module when we declare them. We simply ignore the parameters.
bindPostulatedName :: String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM () Source #
bindPostulatedName builtin q m checks that q is a postulated
name, and binds the builtin builtin to the term m q def,
where def is the current Definition of q.
isUntypedBuiltin :: String -> Bool Source #
bindUntypedBuiltin :: String -> ResolvedName -> TCM () Source #