| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Builtin
Synopsis
- bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
- bindBuiltinNoDef :: BuiltinId -> QName -> TCM ()
- builtinKindOfName :: BuiltinId -> Maybe KindOfName
- bindPostulatedName :: BuiltinId -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
- isUntypedBuiltin :: BuiltinId -> Bool
- bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
Documentation
bindBuiltin :: BuiltinId -> ResolvedName -> TCM () Source #
Bind a builtin thing to an expression.
bindBuiltinNoDef :: BuiltinId -> 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.
builtinKindOfName :: BuiltinId -> Maybe KindOfName Source #
bindPostulatedName :: BuiltinId -> 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 :: BuiltinId -> Bool Source #
bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM () Source #