Captures an LKProof together with the set of previous lemmas used in it.
Attributes
- Companion
- object
- Graph
-
- Supertypes
Members list
Value members
Concrete methods
Inserts the proofs of previous lemmas into its proof.
Inserts the proofs of previous lemmas into its proof.
By default, all lemmas will be included, except those marked with the "nocombine" attribute. To include lemmas marked with "nocombine", use the included parameter. To exclude lemmas that would otherwise be included, use the excluded parameter.
Value parameters
- excluded
-
Proofs for which this evaluates to true will not be included.
- included
-
Proofs for which this is true will be included, unless excluded is also true.
Attributes
The transitive closure of the set of previous lemmas used in the proof of this lemma.
The transitive closure of the set of previous lemmas used in the proof of this lemma.
Attributes
The set of previous lemmas used in the proof of this lemma.
The set of previous lemmas used in the proof of this lemma.