InductionUnfoldingReduction
Attributes
- Source
- inductionReduction.scala
- Graph
-
- Supertypes
Members list
Value members
Concrete methods
Tries to apply the induction unfolding reduction to a given inference.
Tries to apply the induction unfolding reduction to a given inference.
Value parameters
- ctx
-
Defines constants, types, etc.
- proof
-
The induction unfolding reduction is tried to applied to the last inference of this proof.
Attributes
- Returns
-
None if the proof does not end with an induction inference, otherwise see
inductionUnfoldingReduction.apply(InductionRule)(Context): Option[LKProof]. - Source
- inductionReduction.scala
Tries to unfold an induction inference.
Tries to unfold an induction inference.
Value parameters
- ctx
-
Defines constants, types, etc.
- induction
-
The induction inference to be unfolded.
Attributes
- Returns
-
If the given induction's term is in constructor form a proof of the same end-sequent for which the induction inference has been unfolded is returned, otherwise None.
- Source
- inductionReduction.scala
Tries to apply the reduction.
Tries to apply the reduction.
Value parameters
- ctx
-
Defines constants, types, etc.
- induction
-
See
inductionUnfoldingReduction$.apply(induction:InductionRule)(ctx:Context):Option[LKProof]
Attributes
- Returns
-
If the induction rule could be unfolded a proof of the same end-sequent and a sequent connector is returned, otherwise None is returned.
- Source
- inductionReduction.scala
Inherited methods
Attributes
- Inherited from:
- Reduction
- Source
- Reduction.scala
Attributes
- Inherited from:
- Reduction
- Source
- Reduction.scala
Attributes
- Inherited from:
- Reduction
- Source
- Reduction.scala
Implicits
Implicits
Attributes
- Source
- inductionReduction.scala