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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.Builtin

Synopsis

Documentation

bindBuiltin :: String -> Expr -> TCM () Source #

Bind a builtin thing to an expression.

bindBuiltinNoDef :: String -> QName -> TCM () Source #

Bind a builtin thing to a new name.

bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM () Source #

bindPostulatedName builtin e m checks that e is a postulated name q, and binds the builtin builtin to the term m q def, where def is the current Definition of q.