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
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
.
isUntypedBuiltin :: String -> Bool Source
bindUntypedBuiltin :: String -> Expr -> TCM () Source