ImpRightRule

gapt.proofs.lk.rules.ImpRightRule
See theImpRightRule companion class

Attributes

Companion
class
Source
ImpRightRule.scala
Graph
Supertypes
trait Product
trait Mirror
class Object
trait Matchable
class Any
Show all
Self type

Members list

Type members

Inherited types

type MirroredElemLabels <: Tuple

The names of the product elements

The names of the product elements

Attributes

Inherited from:
Mirror
Source
Mirror.scala

The name of the type

The name of the type

Attributes

Inherited from:
Mirror
Source
Mirror.scala

Value members

Concrete methods

def apply(subProof: LKProof, impPremise: IndexOrFormula, impConclusion: IndexOrFormula): ImpRightRule

Convenience constructor for →:r. Each of the aux formulas can be given as an index or a formula. If it is given as a formula, the constructor will attempt to find an appropriate index on its own.

Convenience constructor for →:r. Each of the aux formulas can be given as an index or a formula. If it is given as a formula, the constructor will attempt to find an appropriate index on its own.

Value parameters

impConclusion

Index of the conclusion of the implication or the conclusion itself.

impPremise

Index of the premise of the implication or the premise itself.

subProof

The subproof.

Attributes

Source
ImpRightRule.scala
def apply(subProof: LKProof, mainFormula: Formula): ImpRightRule

Convenience constructor for →:r that, given a proposed main formula A → B, will attempt to create an inference with this main formula.

Convenience constructor for →:r that, given a proposed main formula A → B, will attempt to create an inference with this main formula.

Value parameters

mainFormula

The formula to be inferred. Must be of the form A → B.

subProof

The subproof.

Attributes

Source
ImpRightRule.scala

Inherited methods

def findIndicesOrFormulasInPremise(premise: HOLSequent)(antIndicesFormulas: Seq[IndexOrFormula], sucIndicesFormulas: Seq[IndexOrFormula]): (Seq[Formula], Seq[Int], Seq[Formula], Seq[Int])

Attributes

Inherited from:
ConvenienceConstructor
Source
ConvenienceConstructor.scala

Inherited fields

Attributes

Inherited from:
ConvenienceConstructor
Source
ConvenienceConstructor.scala