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

Safe Haskell | None

Agda.TypeChecking.Rules.Builtin

Synopsis

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

# Documentation

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

Bind a builtin thing to an expression.

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

`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`.