| Safe Haskell | None |
|---|
Agda.TypeChecking.Rules.Builtin
- bindBuiltin :: String -> Expr -> TCM ()
- bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()
Documentation
bindBuiltin :: String -> Expr -> TCM ()Source
Bind a builtin thing to an expression.
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.