Safe Haskell | None |
---|---|
Language | Haskell98 |
- bindBuiltin :: String -> Expr -> TCM ()
- bindBuiltinNoDef :: String -> QName -> TCM ()
- bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()
- isUntypedBuiltin :: String -> Bool
- bindUntypedBuiltin :: String -> Expr -> TCM ()
Documentation
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
.
isUntypedBuiltin :: String -> Bool Source #