Agda-2.3.0: A dependently typed functional programming language and proof assistant
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.
bindPostulatedName builtin e m
m q def
Produced by Haddock version 2.9.4