gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.lk/gapt.proofs.lk.rules/EqualityRule

EqualityRule

gapt.proofs.lk.rules.EqualityRule
See theEqualityRule companion object
abstract class EqualityRule extends UnaryLKProof, CommonRule

Abstract class that performs most of the construction of left and right equality rules.

Attributes

Companion
object
Source
EqualityRule.scala
Graph
Supertypes
trait CommonRule
class UnaryLKProof
class LKProof
trait DagProof[LKProof]
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
Known subtypes

Members list

Value members

Abstract methods

def aux: SequentIndex

Attributes

Source
EqualityRule.scala
def eq: SequentIndex

Attributes

Source
EqualityRule.scala
def replacementContext: Abs

Attributes

Source
EqualityRule.scala
def subProof: LKProof

The immediate subproof of the rule.

The immediate subproof of the rule.

Attributes

Source
EqualityRule.scala

Concrete methods

def auxIndices: Seq[Seq[SequentIndex]]

A list of lists of SequentIndices denoting the auxiliary formula(s) of the rule. The first list contains the auxiliary formulas in the first premise and so on.

A list of lists of SequentIndices denoting the auxiliary formula(s) of the rule. The first list contains the auxiliary formulas in the first premise and so on.

Attributes

Source
EqualityRule.scala
def equation: Formula

Attributes

Source
EqualityRule.scala
override def formulasToBeDeleted: Seq[Seq[SequentIndex]]

Attributes

Definition Classes
Source
EqualityRule.scala
def mainFormula: Formula

Attributes

Source
EqualityRule.scala

Inherited methods

protected def LKRuleCreationException(message: String): LKRuleCreationException

Attributes

Inherited from:
LKProof
Source
LKProof.scala
def auxFormulas: Seq[Seq[Formula]]

A list of lists containing the auxiliary formulas of the rule. The first list constains the auxiliary formulas in the first premise and so on.

A list of lists containing the auxiliary formulas of the rule. The first list constains the auxiliary formulas in the first premise and so on.

Attributes

Inherited from:
SequentProof
Source
SequentProof.scala
def canEqual(that: Any): Boolean

Attributes

Inherited from:
Equals
protected def contexts: Seq[Sequent[Formula]]

Attributes

Inherited from:
ContextRule
Source
SequentProof.scala
def dagLike: DagLikeOps[Proof]

Operations that view the sub-proofs as a DAG, which ignore duplicate sub-proofs, see gapt.proofs.DagProof.DagLikeOps for a list.

Operations that view the sub-proofs as a DAG, which ignore duplicate sub-proofs, see gapt.proofs.DagProof.DagLikeOps for a list.

Attributes

Inherited from:
DagProof
Source
DagProof.scala
def depth: Int

Depth of the proof, which is the maximum length of a path you can take via immediateSubProofs.

Depth of the proof, which is the maximum length of a path you can take via immediateSubProofs.

Attributes

Inherited from:
DagProof
Source
DagProof.scala
final def endSequent: HOLSequent

The end-sequent of the rule.

The end-sequent of the rule.

Attributes

Inherited from:
LKProof
Source
LKProof.scala
override def equals(that: Any): Boolean

Compares the receiver object (this) with the argument object (that) for equivalence.

Compares the receiver object (this) with the argument object (that) for equivalence.

Any implementation of this method should be an equivalence relation:

  • It is reflexive: for any instance x of type Any, x.equals(x) should return true.
  • It is symmetric: for any instances x and y of type Any, x.equals(y) should return true if and only if y.equals(x) returns true.
  • It is transitive: for any instances x, y, and z of type Any if x.equals(y) returns true and y.equals(z) returns true, then x.equals(z) should return true.

If you override this method, you should verify that your implementation remains an equivalence relation. Additionally, when overriding this method it is usually necessary to override hashCode to ensure that objects which are "equal" (o1.equals(o2) returns true) hash to the same scala.Int. (o1.hashCode.equals(o2.hashCode)).

Value parameters

that

the object to compare against this object for equality.

Attributes

Returns

true if the receiver object is equivalent to the argument; false otherwise.

Definition Classes
DagProof -> Equals -> Any
Inherited from:
DagProof
Source
DagProof.scala
def getSequentConnector: SequentConnector

The object connecting the lower and upper sequents.auxFormulas

The object connecting the lower and upper sequents.auxFormulas

Attributes

Inherited from:
UnaryLKProof
Source
UnaryLKProof.scala
override def immediateSubProofs: Seq[LKProof]

The immediate subproofs of this rule.

The immediate subproofs of this rule.

Attributes

Definition Classes
Inherited from:
UnaryLKProof
Source
UnaryLKProof.scala
def longName: String

The name of this rule (in words).

The name of this rule (in words).

Attributes

Inherited from:
DagProof
Source
DagProof.scala
protected def mainFormulaSequent: Sequent[Formula]

Attributes

Inherited from:
ContextRule
Source
SequentProof.scala
def mainFormulas: Seq[Formula]

The list of main formulas of the rule.

The list of main formulas of the rule.

Attributes

Inherited from:
SequentProof
Source
SequentProof.scala
override def mainIndices: Seq[SequentIndex]

A list of SequentIndices denoting the main formula(s) of the rule.

A list of SequentIndices denoting the main formula(s) of the rule.

Attributes

Definition Classes
Inherited from:
ContextRule
Source
SequentProof.scala
def name: String

The name of this rule (in symbols).

The name of this rule (in symbols).

Attributes

Inherited from:
DagProof
Source
DagProof.scala
override def occConnectors: Seq[SequentConnector]

A list of occurrence connectors, one for each immediate subproof.

A list of occurrence connectors, one for each immediate subproof.

Attributes

Definition Classes
Inherited from:
ContextRule
Source
SequentProof.scala
def premise: HOLSequent

The upper sequent of the rule.

The upper sequent of the rule.

Attributes

Inherited from:
UnaryLKProof
Source
UnaryLKProof.scala
def premises: Seq[Sequent[Formula]]

The upper sequents of the rule.

The upper sequents of the rule.

Attributes

Inherited from:
SequentProof
Source
SequentProof.scala
def productArity: Int

Attributes

Inherited from:
Product
def productElement(n: Int): Any

Attributes

Inherited from:
Product
def productElementName(n: Int): String

Attributes

Inherited from:
Product
def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product
def productPrefix: String

Attributes

Inherited from:
Product
override protected def stepString(subProofLabels: Map[Any, String]): String

Attributes

Definition Classes
Inherited from:
SequentProof
Source
SequentProof.scala
def subProofAt(pos: List[Int]): Proof

Returns the subproof at the given position: p.subProofAt(Nil) is p itself; p.subProofAt(i :: is) is the ith subproof of p.subProofAt(is).

Returns the subproof at the given position: p.subProofAt(Nil) is p itself; p.subProofAt(i :: is) is the ith subproof of p.subProofAt(is).

Attributes

Inherited from:
DagProof
Source
DagProof.scala
def subProofs: Set[Proof]

Set of all (transitive) sub-proofs including this.

Set of all (transitive) sub-proofs including this.

Attributes

Inherited from:
DagProof
Source
DagProof.scala
override def toString: String

Returns a string representation of the object.

Returns a string representation of the object.

The default representation is platform dependent.

Attributes

Returns

a string representation of the object.

Definition Classes
DagProof -> Any
Inherited from:
DagProof
Source
DagProof.scala
def treeLike: TreeLikeOps[Proof]

Operations that view the sub-proofs as a tree, see gapt.proofs.DagProof.TreeLikeOps for a list.

Operations that view the sub-proofs as a tree, see gapt.proofs.DagProof.TreeLikeOps for a list.

Attributes

Inherited from:
DagProof
Source
DagProof.scala
final protected def validateIndices(premise: HOLSequent, antecedentIndices: Seq[SequentIndex], succedentIndices: Seq[SequentIndex]): Unit

Checks whether indices are in the right place and premise is defined at all of them.

Checks whether indices are in the right place and premise is defined at all of them.

Value parameters

antecedentIndices

Indices that should be in the antecedent.

premise

The sequent to be checked.

succedentIndices

Indices that should be in the succedent.

Attributes

Inherited from:
LKProof
Source
LKProof.scala

Concrete fields

val auxFormula: Formula

Attributes

Source
EqualityRule.scala
val by: Expr

Attributes

Source
EqualityRule.scala
val leftToRight: Boolean

Attributes

Source
EqualityRule.scala
val what: Expr

Attributes

Source
EqualityRule.scala

Inherited fields

lazy override val conclusion: Sequent[Formula]

The conclusion of the rule.

The conclusion of the rule.

Attributes

Inherited from:
ContextRule
Source
SequentProof.scala
override val hashCode: Int

Calculate a hash code value for the object.

Calculate a hash code value for the object.

The default hashing algorithm is platform dependent.

Note that it is allowed for two objects to have identical hash codes (o1.hashCode.equals(o2.hashCode)) yet not be equal (o1.equals(o2) returns false). A degenerate implementation could always return 0. However, it is required that if two objects are equal (o1.equals(o2) returns true) that they have identical hash codes (o1.hashCode.equals(o2.hashCode)). Therefore, when overriding this method, be sure to verify that the behavior is consistent with the equals method.

Attributes

Returns

the hash code value for this object.

Inherited from:
DagProof
Source
DagProof.scala
Generated with