case class SequentConnector(lowerSizes: (Int, Int), upperSizes: (Int, Int), parentsSequent: Sequent[Seq[SequentIndex]]) extends Product with Serializable
This class models the connection of formula occurrences between two sequents in a proof.
The most basic use case is that of connecting the conclusion of an LK inference with one of the premises. This is the origin of the names "lowerSizes" and "upperSizes".
- lowerSizes
The dimensions of the first ("lower") of the two connected sequents.
- upperSizes
The dimensions of the second ("upper") of the two connected sequents.
- parentsSequent
A sequent of lists of indices such that for each index i of lowerSequent, parentsSequent(i) is the list of indices of the parents of i in upperSequent.
- Source
- SequentConnector.scala
- Alphabetic
- By Inheritance
- SequentConnector
- Serializable
- Product
- Equals
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new SequentConnector(lowerSizes: (Int, Int), upperSizes: (Int, Int), parentsSequent: Sequent[Seq[SequentIndex]])
- lowerSizes
The dimensions of the first ("lower") of the two connected sequents.
- upperSizes
The dimensions of the second ("upper") of the two connected sequents.
- parentsSequent
A sequent of lists of indices such that for each index i of lowerSequent, parentsSequent(i) is the list of indices of the parents of i in upperSequent.
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def *(that: SequentConnector): SequentConnector
Concatenates two SequentConnectors.
Concatenates two SequentConnectors.
- that
An SequentConnector. upperSizes of this must be the same as lowerSizes of that.
- returns
An SequentConnector that connects the lower sequent of this with the upper sequent of that.
- def +(child: SequentIndex, parent: SequentIndex): SequentConnector
Adds a child/parent pair to an SequentConnector.
Adds a child/parent pair to an SequentConnector.
- child
An index of lowerSequent.
- parent
An index of upperSequent.
- returns
A new SequentConnector in which parents(child) contains parent.
- def +(that: SequentConnector): SequentConnector
Forms the union of two SequentConnectors.
Forms the union of two SequentConnectors.
- that
An SequentConnector. Must have the same upper and lower sizes as this.
- returns
A new SequentConnector o such that for any i, o.parents(i) = this.parents(i) ∪ that.parents(i).
- def -(child: SequentIndex, parent: SequentIndex): SequentConnector
Removes a child/parent pair from an SequentConnector.
Removes a child/parent pair from an SequentConnector.
- child
An index of lowerSequent.
- parent
An index of upperSequent. Must be a parent of child.
- returns
A new SequentConnector in which parents(child) no longer contains parent.
- def ->[B](y: B): (SequentConnector, B)
- Implicit
- This member is added by an implicit conversion from SequentConnector toArrowAssoc[SequentConnector] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val antL: Int
- val antU: Int
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def child(idx: SequentIndex): SequentIndex
Given a SequentIndex for the upper sequent, this returns the child of that occurrence in the lower sequent (if there is exactly one).
Given a SequentIndex for the upper sequent, this returns the child of that occurrence in the lower sequent (if there is exactly one).
- idx
An index of upperSequent.
- returns
The unique child of idx.
- def child[T](upperTs: Sequent[T], default: => T = ???): Sequent[T]
- def children[T](upperTs: Sequent[T]): Sequent[Seq[T]]
- def children(idx: SequentIndex): Seq[SequentIndex]
Given a SequentIndex for the upper sequent, this returns the list of children of that occurrence in the lower sequent (if defined).
Given a SequentIndex for the upper sequent, this returns the list of children of that occurrence in the lower sequent (if defined).
- idx
An index of upperSequent.
- returns
The list of children of idx.
- def childrenSequent: Sequent[Seq[SequentIndex]]
Analogous to parentsSequent, but in the other direction.
Analogous to parentsSequent, but in the other direction.
- returns
A sequent of lists of indices such that for each index i of upperSequent, childrenSequent(i) is the list of indices of the children of i in lowerSequent.
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- def ensuring(cond: (SequentConnector) => Boolean, msg: => Any): SequentConnector
- Implicit
- This member is added by an implicit conversion from SequentConnector toEnsuring[SequentConnector] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (SequentConnector) => Boolean): SequentConnector
- Implicit
- This member is added by an implicit conversion from SequentConnector toEnsuring[SequentConnector] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): SequentConnector
- Implicit
- This member is added by an implicit conversion from SequentConnector toEnsuring[SequentConnector] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): SequentConnector
- Implicit
- This member is added by an implicit conversion from SequentConnector toEnsuring[SequentConnector] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- def inv: SequentConnector
Inverts an SequentConnector.
Inverts an SequentConnector.
- returns
This SequentConnector with its lower and upper sizes (and parents and children methods) switched around.
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val lowerSizes: (Int, Int)
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- def parent[T](lowerTs: Sequent[T], default: => T = ???): Sequent[T]
Given a sequent lowerTs of the same size as the lower sequent, return a sequent of the same size as the upper sequent that contains the unique parent of the Ts in lowerTs, or default otherwise.
- def parent(idx: SequentIndex): SequentIndex
Given a SequentIndex for the lower sequent, this returns the parent of that occurrence in the upper sequent (if there is exactly one).
Given a SequentIndex for the lower sequent, this returns the parent of that occurrence in the upper sequent (if there is exactly one).
- idx
An index of lowerSequent.
- returns
The unique parent of idx.
- def parentOption(idx: SequentIndex): Option[SequentIndex]
Given a SequentIndex for the lower sequent, this returns the parent of that occurrence in the upper sequent (if there is exactly one), and None otherwise.
Given a SequentIndex for the lower sequent, this returns the parent of that occurrence in the upper sequent (if there is exactly one), and None otherwise.
- idx
An index of lowerSequent.
- returns
The unique parent of idx.
- def parents[T](lowerTs: Sequent[T]): Sequent[Seq[T]]
Given a sequent lowerTs of the same size as the lower sequent, return a sequent of the same size as the upper sequent that contains the parents of the Ts in lowerTs.
Given a sequent lowerTs of the same size as the lower sequent, return a sequent of the same size as the upper sequent that contains the parents of the Ts in lowerTs.
If we call the returned sequent upperTs, then lowerTs(i) in upperTs(j) for all j in parents(i).
The intended use-case is that lowerTs is a sequent of labels for the formulas in the lower sequent. parents(lowerTs) will then contain the correct labels for the formulas in the upper sequent.
- def parents(idx: SequentIndex): Seq[SequentIndex]
Given a SequentIndex for the lower sequent, this returns the list of parents of that occurrence in the upper sequent (if defined).
Given a SequentIndex for the lower sequent, this returns the list of parents of that occurrence in the upper sequent (if defined).
- idx
An index of lowerSequent.
- returns
The list of parents of idx.
- val parentsSequent: Sequent[Seq[SequentIndex]]
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val sucL: Int
- val sucU: Int
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- val upperSizes: (Int, Int)
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Shadowed Implicit Value Members
- def +(other: String): String
- Implicit
- This member is added by an implicit conversion from SequentConnector toany2stringadd[SequentConnector] performed by method any2stringadd in scala.Predef.
- Shadowing
- This implicitly inherited member is shadowed by one or more members in this class.
To access this member you can use a type ascription:(sequentConnector: any2stringadd[SequentConnector]).+(other)
- Definition Classes
- any2stringadd
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from SequentConnector toStringFormat[SequentConnector] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @deprecated @inline()
- Deprecated
(Since version 2.12.16) Use
formatString.format(value)instead ofvalue.formatted(formatString), or use thef""string interpolator. In Java 15 and later,formattedresolves to the new method in String which has reversed parameters.
- def →[B](y: B): (SequentConnector, B)
- Implicit
- This member is added by an implicit conversion from SequentConnector toArrowAssoc[SequentConnector] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.
This is the API documentation for GAPT.
The main package is gapt.