Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 #