Lurch core classes

Class

Environment

An Environment in Lurch is a wrapper that can enclose any sequence of LogicConcepts, which is useful for many purposes, including the following.

  • Nesting subproofs within a proof so that it is clear where assumptions and variable declarations are (and are not) in force. (This is what we anticipate as the most common use.)
  • Marking the boundaries of theorems, proofs, definitions, axioms, and other important structures that form a single, cohesive unit.
  • Delimiting exercises in a text from the rest of the text, so that variables declared in those exercises do not remain in scope for the rest of the text.

This class inherits its constructor from its parent class; to create an environment wrapping a sequence L_1 through L_n of LogicConcepts, just call new Environment( L1, ..., Ln ). Such an environment does not, by default, declare or bind any new symbols. But you can create an instance of the Binding Environment subclass to do so; it is useful, for example, when constructing subproofs that begin by declaring some symbol arbitrary. See its documentation for further details.

Constructor

new Environment()

Source

Methods

conclusions()

Any LogicConcept can be marked as a "given," meaning that it is to be seen as a hypothesis/assumption within its context. Any LogicConcept not so marked is viewed as a "claim," meaning that it is an assertion/statement of truth, within its context. For this, we use the attribute functions built into the MathConcept class, including isA(), asA(), and so on.

The conclusions of a LogicConcept include:

  • all of its children that are claim Expressions
  • all of the conclusions in any of its child Environments that are themselves claims, recursively

Thus conclusions are always Expressions or Declarations, never other Environments. And for each one, all the members of its ancestor chain, up to but not necessarily including the Environment in which this method was called, will be claims, not givens.

Source