Safe Haskell | None |
---|
- 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
.