| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Rules.Builtin
- bindBuiltin :: String -> Expr -> TCM ()
- bindBuiltinNoDef :: String -> QName -> TCM ()
- bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()
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.