InductionCase
gapt.proofs.lk.rules.InductionCase
case class InductionCase(proof: LKProof, constructor: Const, hypotheses: Seq[SequentIndex], eigenVars: Seq[Var], conclusion: SequentIndex)
Proof that a given data type constructor c preserves a formula F:
(π) F(x,,1,,), F(x,,2,,), ..., F(x,,n,,), Γ :- Δ, F(c(x,,1,,,...,x,,n,,,y,,1,,,...,y,,n,,))
The variables x,,i,, and y,,i,, are eigenvariables; x,,i,, are the eigenvariables of the same type as the inductive data type, y,,i,, are the other arguments of the constructor c. They can come in any order in the constructor.
Value parameters
- conclusion
-
Index of F(c(x,,1,,,...,x,,n,,,y,,1,,,...,y,,n,,))
- constructor
-
The constructor c of the inductive data type that we're considering.
- eigenVars
-
The eigenvariables of this case: x,,1,,, ..., x,,n,,, y,,1,,, ..., y,,n,, (these need to correspond to the order in c)
- hypotheses
-
Indices of F(x,,1,,), ..., F(x,,n,,)
- proof
-
The LKProof ending in the sequent of this case.
Attributes
- Source
- InductionCase.scala
- Graph
-
- Supertypes
Members list
In this article