bind package:Agda
bind n f provides f with a fresh variable, which can
be used in any extended context.
Returns an Abs which binds the extra variable.
Bind a defined name. Must not shadow anything.
Bind a name. Returns the
TypeError if exists, but does not
throw it.
Bind a qualified module name. Adds it to the imports field of the
scope.
After collecting some variable names in the scopeVarsToBind, bind them
all simultaneously.
Add one (more) relation symbol to the rewrite relations.
Like bind but returns a bare term.
Bind a builtin thing to an expression.
Bind a builtin thing to a new name.
Since their type is closed, it does not matter whether we are in a
parameterized module when we declare them. We simply ignore the
parameters.
bindPostulatedName builtin q m checks that
q is a
postulated name, and binds the builtin
builtin to the term
m q def, where
def is the current
Definition
of
q.