Agda.TypeChecking.Rules.Builtin

Documentation

bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()

Bind a builtin thing to an expression.

bindBuiltinNoDef :: BuiltinId -> QName -> TCM ()

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

bindPostulatedName :: BuiltinId -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()

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

bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()