gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.lk/LKVisitor

LKVisitor

gapt.proofs.lk.LKVisitor
trait LKVisitor[T]

Implementation of the visitor pattern for gapt.proofs.lk.LKProof. Proof transformations can implement this trait to reduce boilerplate code.

Type parameters

T

Type of additional arguments that may be used in the transformation.

Attributes

Source
LKVisitor.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
object CreateASchemaVersion.type

Members list

Value members

Concrete methods

final def apply(proof: LKProof, otherArg: T): 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.

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.

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

Attributes

Source
LKVisitor.scala
protected def recurse(proof: LKProof, otherArg: T): (LKProof, SequentConnector)

Attributes

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

Attributes

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

Attributes

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

Attributes

Source
LKVisitor.scala
protected def visitBottomAxiom(otherArg: T): (LKProof, SequentConnector)

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

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

Attributes

Source
LKVisitor.scala
protected def visitOpenAssumption(proof: OpenAssumption, otherArg: T): (LKProof, SequentConnector)

Attributes

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

Attributes

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

Attributes

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

Attributes

Source
LKVisitor.scala
protected def visitTopAxiom(otherArg: T): (LKProof, SequentConnector)

Attributes

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

Attributes

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

Attributes

Source
LKVisitor.scala
final def withSequentConnector(proof: LKProof, otherArg: T): (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.

Source
LKVisitor.scala
Generated with