gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.gaptic/ProofState/ProofSegmentInsertionVisitor

ProofSegmentInsertionVisitor

gapt.proofs.gaptic.ProofState.ProofSegmentInsertionVisitor
class ProofSegmentInsertionVisitor(failOnMissingSubgoal: Boolean) extends LKVisitor[Unit]

Attributes

Source
core.scala
Graph
Supertypes
trait LKVisitor[Unit]
class Object
trait Matchable
class Any

Members list

Value members

Concrete methods

override def visitOpenAssumption(p: OpenAssumption, dummy: Unit): (LKProof, SequentConnector)

Attributes

Definition Classes
Source
core.scala

Inherited methods

final def apply(proof: LKProof, otherArg: Unit): LKProof

Applies the proof transformation to an LKProof.

Applies the proof transformation to an LKProof.

Value parameters

proof

The input proof.

Attributes

Returns

The transformed proof.

Inherited from:
LKVisitor
Source
LKVisitor.scala
def contractAfter[A](visitingFunction: (LKProof, A) => (LKProof, SequentConnector)): (LKProof, A) => (LKProof, SequentConnector)

Transforms a visiting function by inserting contractions after it. Only formula occurrences that were not in the old proof -- i.e., that have been added by the visitor -- are contracted.

Transforms a visiting function by inserting contractions after it. Only formula occurrences that were not in the old proof -- i.e., that have been added by the visitor -- are contracted.

Value parameters

visitingFunction

The visiting function after which contractions should be inserted. In most cases, just using recurse here should be fine.

Attributes

Returns

A new visiting function that behaves the same as the old one, but contracts all duplicate new formulas at the end.

Inherited from:
LKVisitor
Source
LKVisitor.scala
def one2one(proof: LKProof, arg: Unit)(func: Seq[(LKProof, SequentConnector)] => LKProof): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def recurse(proof: LKProof, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
def transportToSubProof(arg: Unit, proof: LKProof, subProofIdx: Int): T

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitAndLeft(proof: AndLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitAndRight(proof: AndRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitBottomAxiom(otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitContractionLeft(proof: ContractionLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitContractionRight(proof: ContractionRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitCut(proof: CutRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitDefinitionLeft(proof: ConversionLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitDefinitionRight(proof: ConversionRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitEqualityLeft(proof: EqualityLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitEqualityRight(proof: EqualityRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitExistsLeft(proof: ExistsLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitExistsRight(proof: ExistsRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitExistsSkLeft(proof: ExistsSkLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitForallLeft(proof: ForallLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitForallRight(proof: ForallRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitForallSkRight(proof: ForallSkRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitImpLeft(proof: ImpLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitImpRight(proof: ImpRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitInduction(proof: InductionRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitLogicalAxiom(proof: LogicalAxiom, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitNegLeft(proof: NegLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitNegRight(proof: NegRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitOrLeft(proof: OrLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitOrRight(proof: OrRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitReflexivityAxiom(proof: ReflexivityAxiom, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitTopAxiom(otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitWeakeningLeft(proof: WeakeningLeftRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
protected def visitWeakeningRight(proof: WeakeningRightRule, otherArg: Unit): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
def withIdentitySequentConnector(proof: LKProof): (LKProof, SequentConnector)

Attributes

Inherited from:
LKVisitor
Source
LKVisitor.scala
final def withSequentConnector(proof: LKProof, otherArg: Unit): (LKProof, SequentConnector)

Applies the proof transformation to an LKProof.

Applies the proof transformation to an LKProof.

Value parameters

proof

The input proof.

Attributes

Returns

Transformed proof, and the sequent connector with the new proof as lower sequent and the old proof as upper sequent.

Inherited from:
LKVisitor
Source
LKVisitor.scala
Generated with