Constructor
new BindingEnvironment(…args)
Construct a new BindingEnvironment instance from the given array of bound variables (one or more Symbols) and body (required Environment). Recall from the documentation of the BindingInterface that bindings do not contain an operator, but BindingEnvironments typically do not want one, so there is not always a need to wrap the resulting object in a larger LogicConcept.
For example, when encoding something like a subproof that treats $x$ as an arbitrary variable and eventually proves some expression $P$ containing $x$, we might use a BindingEnvironment like the following to represent it.
new BindingEnvironment(
new LurchSymbol( 'x' ),
new Environment(
step1, // some Expression
step2, // some Expression
// and so on, eventually reaching the expression:
P
)
)
Note that while it is possible later to remove children from a BindingEnvironment so that it does not have the required structure of symbols-then-body, this is almost certain to result in the members of this class malfunctioning or throwing errors. Clients should not remove the necessary children of a BindingEnvironment; that is not supported.
Although it is unnecessarily to repeat the same variable twice on the list of bound variables, we do not explicitly forbid it.
Parameters
-
args
LogicConcept
<repeatable>
the list of one or more Symbols that this environment binds, followed by its body, which must be of type Environment.
Throws
This constructor throws an error if any argument is not a LogicConcept, or if any argument but the last is not a Symbols, or the last argument is not an Environment, or if the list of bound symbols is empty.