Packages

case class Sequent[+A](antecedent: Vector[A], succedent: Vector[A]) extends Product with Serializable

A sequent is a pair of sequences of elements of type A, typically written as a1,…,am :- b1,…,bn.

A

The type of the elements of the sequent.

antecedent

The first list.

succedent

The second list.

Source
sequents.scala
Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Sequent
  2. Serializable
  3. Product
  4. Equals
  5. AnyRef
  6. Any
Implicitly
  1. by RichClause
  2. by RichFOLSequent
  3. by RichFormulaSequent
  4. by labelledSequentToSequent
  5. by any2stringadd
  6. by StringFormat
  7. by Ensuring
  8. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new Sequent(antecedent: Vector[A], succedent: Vector[A])

    antecedent

    The first list.

    succedent

    The second list.

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from Sequent[A] toany2stringadd[Sequent[A]] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ++[B >: A](that: Sequent[B]): Sequent[B]
  5. def ++:[B >: A](es: Iterable[B]): Sequent[B]

    Adds a sequent of elements to the antecedent.

    Adds a sequent of elements to the antecedent. New elements are always outermost, i.e. on the very left.

    es

    A collection of elements of type B > A.

    returns

    The sequent with es added to the antecedent.

  6. def +:[B >: A](e: B): Sequent[B]

    Adds an element to the antecedent.

    Adds an element to the antecedent. New elements are always outermost, i.e. on the very left.

    e

    An element of type B > A

    returns

    The sequent with e added to the antecedent

  7. def ->[B](y: B): (Sequent[A], B)
    Implicit
    This member is added by an implicit conversion from Sequent[A] toArrowAssoc[Sequent[A]] performed by method ArrowAssoc in scala.Predef.This conversion will take place only if A is a subclass of LabelledFormula with FOLFormula (A <: LabelledFormula with FOLFormula).
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  8. def :+[B >: A](e: B): Sequent[B]

    Adds an element to the succedent.

    Adds an element to the succedent. New elements are always outermost, i.e. on the very right.

    e

    An element of type B > A

    returns

    The sequent with e added to the succedent

  9. def :++[B >: A](es: Iterable[B]): Sequent[B]

    Adds a sequence of elements to the succedent.

    Adds a sequence of elements to the succedent. New elements are always outermost, i.e. on the very right.

    es

    A collection of elements of type B > A.

    returns

    The sequent with es added to the succedent.

  10. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  11. val antecedent: Vector[A]
  12. def apply(is: Seq[SequentIndex]): Seq[A]
  13. def apply(i: SequentIndex): A

    Returns the element at some SequentIndex.

    Returns the element at some SequentIndex.

    i

    A SequentIndex, i.e. Ant(k) or Suc(k)

    returns

    The k-th element of the antecedent or succedent, depending on the type of i.

  14. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  15. def cedent(polarity: Polarity): Vector[A]
  16. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  17. def collect[B](f: PartialFunction[A, B]): Sequent[B]
  18. def contains[B](el: B, polarity: Polarity): Boolean
  19. def contains[B](el: B): Boolean

    Returns true iff the sequent contains some element in either cedent.

  20. def delete(is: SequentIndex*)(implicit d: DummyImplicit): Sequent[A]
  21. def delete(is: Seq[SequentIndex]): Sequent[A]
  22. def delete(i: SequentIndex): Sequent[A]
  23. def diff[B >: A](other: Sequent[B]): Sequent[A]

    Takes the multiset difference between two sequents, i.e.

    Takes the multiset difference between two sequents, i.e. each side separately.

  24. def distinct: Sequent[A]

    Removes duplicate formulas from both cedents.

  25. def elements: Vector[A]

    Sequence of elements of the sequent.

    Sequence of elements of the sequent.

    returns

    Antecedent concatenated with succedent.

  26. def ensuring(cond: (Sequent[A]) => Boolean, msg: => Any): Sequent[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toEnsuring[Sequent[A]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  27. def ensuring(cond: (Sequent[A]) => Boolean): Sequent[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toEnsuring[Sequent[A]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  28. def ensuring(cond: Boolean, msg: => Any): Sequent[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toEnsuring[Sequent[A]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  29. def ensuring(cond: Boolean): Sequent[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toEnsuring[Sequent[A]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  30. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  31. def exists(p: (A) => Boolean): Boolean
  32. def filter(p: (A) => Boolean): Sequent[A]

    The sub-sequent of elements satisfying some predicate.

    The sub-sequent of elements satisfying some predicate.

    p

    A function of type A => Boolean.

    returns

    The sequent consisting of only those elements satisfying p.

  33. def filterNot(p: (A) => Boolean): Sequent[A]

    The sub-sequent of elements not satisfying some predicate.

    The sub-sequent of elements not satisfying some predicate.

    p

    A function of type A => Boolean.

    returns

    The sequent consisting of only those elements not satisfying p.

  34. def find(pred: (A) => Boolean): Option[SequentIndex]
  35. def flatMap[B](f: (A) => IterableOnce[B], g: (A) => IterableOnce[B]): Sequent[B]
  36. def flatMap[B](f: (A) => IterableOnce[B]): Sequent[B]
  37. def focus(i: SequentIndex): (A, Sequent[A])

    Focuses on one element of the sequent, i.e.

    Focuses on one element of the sequent, i.e. returns element at index and the rest of the sequent.

    i

    A SequentIndex.

    returns

    A pair consisting of this(i) and the rest of this.

  38. def forall(p: (A) => Boolean): Boolean
  39. def foreach[U](f: (A) => U): Unit
  40. def formulas: Vector[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Definition Classes
    RichFormulaSequent
  41. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  42. def groupBy[B](f: (A) => B): Sequent[(B, Vector[A])]
  43. def indexOf[B >: A](elem: B, polarity: Polarity): SequentIndex
  44. def indexOf[B >: A](elem: B): SequentIndex
  45. def indexOfInAnt[B >: A](elem: B): SequentIndex
  46. def indexOfInSuc[B >: A](elem: B): SequentIndex
  47. def indexOfOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
  48. def indexOfOption[B >: A](elem: B): Option[SequentIndex]
  49. def indices: Vector[SequentIndex]

    Returns the range of indices of the sequent as a sequence.

  50. def indicesSequent: Sequent[SequentIndex]

    Returns the range of indices of the sequent as a sequent.

  51. def indicesWhere(p: (A) => Boolean): Vector[SequentIndex]

    Returns the list of indices of elements satisfying some predicate.

    Returns the list of indices of elements satisfying some predicate.

    p

    A function of type A => Boolean.

  52. def indicesWherePol(p: (A) => Boolean, pol: Polarity): Vector[SequentIndex]
  53. def insertAt[B >: A](i: SequentIndex, el: B): Sequent[B]
  54. def intersect[B >: A](other: Sequent[B]): Sequent[A]

    Computes the intersection of two sequents.

  55. def isDefinedAt(i: SequentIndex): Boolean

    Tests whether the sequent is defined at the supplied SequentIndex.

  56. def isEmpty: Boolean

    Returns true iff both cedents are empty.

  57. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  58. def isSubMultisetOf[B >: A](other: Sequent[B]): Boolean
  59. def isSubsetOf[B >: A](other: Sequent[B]): Boolean

    other

    Another Sequent.

    returns

    True iff other contains this pair of sets.

  60. def isTaut: Boolean
  61. def length: Int

    The number of elements in the sequent.

  62. def lengths: (Int, Int)

    A pair consisting of the lengths of the cedents.

  63. def map[B](f: (A) => B, g: (A) => B): Sequent[B]

    Maps two functions over the antecedent and succedent, respectively.

    Maps two functions over the antecedent and succedent, respectively.

    B

    The return type of f and g.

    f

    The function to map over the antecedent.

    g

    The function to map over the succedent.

    returns

    The sequent of type B that results from mapping f and g over the antecedent and succedent, respectively.

  64. def map[B](f: (A) => B): Sequent[B]

    Maps a function over both cedents

    Maps a function over both cedents

    B

    The return type of f

    f

    A function of type A => B

    returns

    The sequent of type B that results from mapping f over both cedents.

  65. def multiSetEquals[B](other: Sequent[B]): Boolean

    Equality treating each side of the sequent as a multiset.

  66. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  67. def negative: Vector[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichClause[A] performed by method RichClause in gapt.proofs.
    Definition Classes
    RichClause
  68. def nonEmpty: Boolean
  69. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  70. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  71. def polarizedElements: Vector[(A, Polarity)]

    Sequence of elements together with polarities of type Boolean signifying whether an element is in the antecedent or succedent.

  72. def positive: Vector[A]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichClause[A] performed by method RichClause in gapt.proofs.
    Definition Classes
    RichClause
  73. def productElementNames: Iterator[String]
    Definition Classes
    Product
  74. def removeFromAntecedent[B](e: B): Sequent[A]
  75. def removeFromSuccedent[B](e: B): Sequent[A]
  76. def replaceAt[B >: A](i: SequentIndex, el: B): Sequent[B]
  77. def setEquals[B](other: Sequent[B]): Boolean

    Equality treating each side of the sequent as a set.

  78. def size: Int

    Synonym for length.

  79. def sizes: (Int, Int)

    Synonym for lengths.

  80. def sortBy[B](f: (A) => B)(implicit ord: Ordering[B]): Sequent[A]
  81. def sorted[B >: A](implicit ordering: Ordering[B]): Sequent[A]
  82. val succedent: Vector[A]
  83. def swapped: Sequent[A]
  84. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  85. def tautFormula: Option[A]
  86. def tautFormulas: Vector[A]
  87. def toSigRelativeString(implicit sig: BabelSignature): String
  88. def toString(): String
    Definition Classes
    Sequent → AnyRef → Any
  89. def toTuple: (Vector[A], Vector[A])

    returns

    The sequent in tuple form.

  90. def updated[B >: A](updates: Iterable[(SequentIndex, B)]): Sequent[B]
  91. def updated[B >: A](index: SequentIndex, elem: B): Sequent[B]
  92. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  93. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  94. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  95. def withFilter(p: (A) => Boolean): Sequent[A]
  96. def zip[B](that: Sequent[B]): Sequent[(A, B)]
  97. def zipWithIndex: Sequent[(A, SequentIndex)]

Shadowed Implicit Value Members

  1. def ++[B >: A](that: Sequent[B]): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).++(that)
  2. def ++:[B >: A](es: Iterable[B]): Sequent[B]

    Adds a sequent of elements to the antecedent.

    Adds a sequent of elements to the antecedent. New elements are always outermost, i.e. on the very left.

    es

    A collection of elements of type B > A.

    returns

    The sequent with es added to the antecedent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).++:(es)
  3. def +:[B >: A](e: B): Sequent[B]

    Adds an element to the antecedent.

    Adds an element to the antecedent. New elements are always outermost, i.e. on the very left.

    e

    An element of type B > A

    returns

    The sequent with e added to the antecedent

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).+:(e)
  4. def :+[B >: A](e: B): Sequent[B]

    Adds an element to the succedent.

    Adds an element to the succedent. New elements are always outermost, i.e. on the very right.

    e

    An element of type B > A

    returns

    The sequent with e added to the succedent

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).:+(e)
  5. def :++[B >: A](es: Iterable[B]): Sequent[B]

    Adds a sequence of elements to the succedent.

    Adds a sequence of elements to the succedent. New elements are always outermost, i.e. on the very right.

    es

    A collection of elements of type B > A.

    returns

    The sequent with es added to the succedent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).:++(es)
  6. val antecedent: Vector[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).antecedent
  7. def apply(is: Seq[SequentIndex]): Seq[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).apply(is)
  8. def apply(i: SequentIndex): Formula

    Returns the element at some SequentIndex.

    Returns the element at some SequentIndex.

    i

    A SequentIndex, i.e. Ant(k) or Suc(k)

    returns

    The k-th element of the antecedent or succedent, depending on the type of i.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).apply(i)
  9. def cedent(polarity: Polarity): Vector[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).cedent(polarity)
  10. def collect[B](f: PartialFunction[Formula, B]): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).collect(f)
  11. def contains[B](el: B, polarity: Polarity): Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).contains(el, polarity)
  12. def contains[B](el: B): Boolean

    Returns true iff the sequent contains some element in either cedent.

    Returns true iff the sequent contains some element in either cedent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).contains(el)
  13. def delete(is: SequentIndex*)(implicit d: DummyImplicit): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).delete(is)(d)
  14. def delete(is: Seq[SequentIndex]): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).delete(is)
  15. def delete(i: SequentIndex): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).delete(i)
  16. def diff[B >: A](other: Sequent[B]): Sequent[Formula]

    Takes the multiset difference between two sequents, i.e.

    Takes the multiset difference between two sequents, i.e. each side separately.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).diff(other)
  17. def distinct: Sequent[Formula]

    Removes duplicate formulas from both cedents.

    Removes duplicate formulas from both cedents.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).distinct
  18. def elements: Vector[Formula]

    Sequence of elements of the sequent.

    Sequence of elements of the sequent.

    returns

    Antecedent concatenated with succedent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).elements
  19. def exists(p: (Formula) => Boolean): Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).exists(p)
  20. def filter(p: (Formula) => Boolean): Sequent[Formula]

    The sub-sequent of elements satisfying some predicate.

    The sub-sequent of elements satisfying some predicate.

    p

    A function of type A => Boolean.

    returns

    The sequent consisting of only those elements satisfying p.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).filter(p)
  21. def filterNot(p: (Formula) => Boolean): Sequent[Formula]

    The sub-sequent of elements not satisfying some predicate.

    The sub-sequent of elements not satisfying some predicate.

    p

    A function of type A => Boolean.

    returns

    The sequent consisting of only those elements not satisfying p.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).filterNot(p)
  22. def find(pred: (Formula) => Boolean): Option[SequentIndex]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).find(pred)
  23. def flatMap[B](f: (Formula) => IterableOnce[B], g: (Formula) => IterableOnce[B]): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).flatMap(f, g)
  24. def flatMap[B](f: (Formula) => IterableOnce[B]): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).flatMap(f)
  25. def focus(i: SequentIndex): (Formula, Sequent[Formula])

    Focuses on one element of the sequent, i.e.

    Focuses on one element of the sequent, i.e. returns element at index and the rest of the sequent.

    i

    A SequentIndex.

    returns

    A pair consisting of this(i) and the rest of this.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).focus(i)
  26. def forall(p: (Formula) => Boolean): Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).forall(p)
  27. def foreach[U](f: (Formula) => U): Unit
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).foreach(f)
  28. def groupBy[B](f: (Formula) => B): Sequent[(B, Vector[Formula])]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).groupBy(f)
  29. def indexOf[B >: A](elem: B, polarity: Polarity): SequentIndex
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOf(elem, polarity)
  30. def indexOf[B >: A](elem: B): SequentIndex
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOf(elem)
  31. def indexOfInAnt[B >: A](elem: B): SequentIndex
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfInAnt(elem)
  32. def indexOfInSuc[B >: A](elem: B): SequentIndex
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfInSuc(elem)
  33. def indexOfOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfOption(elem, pol)
  34. def indexOfOption[B >: A](elem: B): Option[SequentIndex]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfOption(elem)
  35. def indices: Vector[SequentIndex]

    Returns the range of indices of the sequent as a sequence.

    Returns the range of indices of the sequent as a sequence.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indices
  36. def indicesSequent: Sequent[SequentIndex]

    Returns the range of indices of the sequent as a sequent.

    Returns the range of indices of the sequent as a sequent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indicesSequent
  37. def indicesWhere(p: (Formula) => Boolean): Vector[SequentIndex]

    Returns the list of indices of elements satisfying some predicate.

    Returns the list of indices of elements satisfying some predicate.

    p

    A function of type A => Boolean.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indicesWhere(p)
  38. def indicesWherePol(p: (Formula) => Boolean, pol: Polarity): Vector[SequentIndex]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indicesWherePol(p, pol)
  39. def insertAt[B >: A](i: SequentIndex, el: B): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).insertAt(i, el)
  40. def intersect[B >: A](other: Sequent[B]): Sequent[Formula]

    Computes the intersection of two sequents.

    Computes the intersection of two sequents.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).intersect(other)
  41. def isDefinedAt(i: SequentIndex): Boolean

    Tests whether the sequent is defined at the supplied SequentIndex.

    Tests whether the sequent is defined at the supplied SequentIndex.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).isDefinedAt(i)
  42. def isEmpty: Boolean

    Returns true iff both cedents are empty.

    Returns true iff both cedents are empty.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).isEmpty
  43. def isSubMultisetOf[B >: A](other: Sequent[B]): Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).isSubMultisetOf(other)
  44. def isSubsetOf[B >: A](other: Sequent[B]): Boolean

    other

    Another Sequent.

    returns

    True iff other contains this pair of sets.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).isSubsetOf(other)
  45. def isTaut: Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).isTaut
  46. def length: Int

    The number of elements in the sequent.

    The number of elements in the sequent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).length
  47. def lengths: (Int, Int)

    A pair consisting of the lengths of the cedents.

    A pair consisting of the lengths of the cedents.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).lengths
  48. def map[B](f: (Formula) => B, g: (Formula) => B): Sequent[B]

    Maps two functions over the antecedent and succedent, respectively.

    Maps two functions over the antecedent and succedent, respectively.

    B

    The return type of f and g.

    f

    The function to map over the antecedent.

    g

    The function to map over the succedent.

    returns

    The sequent of type B that results from mapping f and g over the antecedent and succedent, respectively.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).map(f, g)
  49. def map[B](f: (Formula) => B): Sequent[B]

    Maps a function over both cedents

    Maps a function over both cedents

    B

    The return type of f

    f

    A function of type A => B

    returns

    The sequent of type B that results from mapping f over both cedents.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).map(f)
  50. def multiSetEquals[B](other: Sequent[B]): Boolean

    Equality treating each side of the sequent as a multiset.

    Equality treating each side of the sequent as a multiset.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).multiSetEquals(other)
  51. def nonEmpty: Boolean
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).nonEmpty
  52. def polarizedElements: Vector[(Formula, Polarity)]

    Sequence of elements together with polarities of type Boolean signifying whether an element is in the antecedent or succedent.

    Sequence of elements together with polarities of type Boolean signifying whether an element is in the antecedent or succedent.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).polarizedElements
  53. def productElementNames: Iterator[String]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).productElementNames
    Definition Classes
    Product
  54. def removeFromAntecedent[B](e: B): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).removeFromAntecedent(e)
  55. def removeFromSuccedent[B](e: B): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).removeFromSuccedent(e)
  56. def replaceAt[B >: A](i: SequentIndex, el: B): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).replaceAt(i, el)
  57. def setEquals[B](other: Sequent[B]): Boolean

    Equality treating each side of the sequent as a set.

    Equality treating each side of the sequent as a set.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).setEquals(other)
  58. def size: Int

    Synonym for length.

    Synonym for length.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).size
  59. def sizes: (Int, Int)

    Synonym for lengths.

    Synonym for lengths.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).sizes
  60. def sortBy[B](f: (Formula) => B)(implicit ord: Ordering[B]): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).sortBy(f)(ord)
  61. def sorted[B >: A](implicit ordering: Ordering[B]): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).sorted(ordering)
  62. val succedent: Vector[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).succedent
  63. def swapped: Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).swapped
  64. def tautFormula: Option[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).tautFormula
  65. def tautFormulas: Vector[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).tautFormulas
  66. def toConjunction: FOLFormula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFOLSequent performed by method RichFOLSequent in gapt.proofs.This conversion will take place only if A is a subclass of FOLFormula (A <: FOLFormula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFOLSequent).toConjunction
    Definition Classes
    RichFOLSequent
  67. def toConjunction: Formula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFormulaSequent).toConjunction
    Definition Classes
    RichFormulaSequent
  68. def toDisjunction: FOLFormula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFOLSequent performed by method RichFOLSequent in gapt.proofs.This conversion will take place only if A is a subclass of FOLFormula (A <: FOLFormula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFOLSequent).toDisjunction
    Definition Classes
    RichFOLSequent
  69. def toDisjunction: Formula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFormulaSequent).toDisjunction
    Definition Classes
    RichFormulaSequent
  70. def toFormula: FOLFormula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFOLSequent performed by method RichFOLSequent in gapt.proofs.This conversion will take place only if A is a subclass of FOLFormula (A <: FOLFormula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFOLSequent).toFormula
    Definition Classes
    RichFOLSequent
  71. def toFormula: Formula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFormulaSequent).toFormula
    Definition Classes
    RichFormulaSequent
  72. def toImplication: FOLFormula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFOLSequent performed by method RichFOLSequent in gapt.proofs.This conversion will take place only if A is a subclass of FOLFormula (A <: FOLFormula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFOLSequent).toImplication
    Definition Classes
    RichFOLSequent
  73. def toImplication: Formula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFormulaSequent).toImplication
    Definition Classes
    RichFormulaSequent
  74. def toNegConjunction: FOLFormula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFOLSequent performed by method RichFOLSequent in gapt.proofs.This conversion will take place only if A is a subclass of FOLFormula (A <: FOLFormula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFOLSequent).toNegConjunction
    Definition Classes
    RichFOLSequent
  75. def toNegConjunction: Formula
    Implicit
    This member is added by an implicit conversion from Sequent[A] toRichFormulaSequent performed by method RichFormulaSequent in gapt.proofs.This conversion will take place only if A is a subclass of Formula (A <: Formula).
    Shadowing
    This implicitly inherited member is ambiguous. One or more implicitly inherited members have similar signatures, so calling this member may produce an ambiguous implicit conversion compiler error.
    To access this member you can use a type ascription:
    (sequent: RichFormulaSequent).toNegConjunction
    Definition Classes
    RichFormulaSequent
  76. def toSigRelativeString(implicit sig: BabelSignature): String
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).toSigRelativeString(sig)
  77. def toString(): String
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).toString()
    Definition Classes
    Sequent → AnyRef → Any
  78. def toTuple: (Vector[Formula], Vector[Formula])

    returns

    The sequent in tuple form.

    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).toTuple
  79. def updated[B >: A](updates: Iterable[(SequentIndex, B)]): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).updated(updates)
  80. def updated[B >: A](index: SequentIndex, elem: B): Sequent[B]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).updated(index, elem)
  81. def withFilter(p: (Formula) => Boolean): Sequent[Formula]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).withFilter(p)
  82. def zip[B](that: Sequent[B]): Sequent[(Formula, B)]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).zip(that)
  83. def zipWithIndex: Sequent[(Formula, SequentIndex)]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).zipWithIndex

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated
  2. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from Sequent[A] toStringFormat[Sequent[A]] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @deprecated @inline()
    Deprecated

    (Since version 2.12.16) Use formatString.format(value) instead of value.formatted(formatString), or use the f"" string interpolator. In Java 15 and later, formatted resolves to the new method in String which has reversed parameters.

  3. def indexOfPol[B >: A](elem: B, polarity: Polarity): SequentIndex
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfPol(elem, polarity)
    Annotations
    @deprecated
    Deprecated

    (Since version 2.9) Use indexOf instead.

  4. def indexOfPol[B >: A](elem: B, polarity: Polarity): SequentIndex
    Annotations
    @deprecated
    Deprecated

    (Since version 2.9) Use indexOf instead.

  5. def indexOfPolOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
    Implicit
    This member is added by an implicit conversion from Sequent[A] toSequent[Formula] performed by method labelledSequentToSequent in gapt.proofs.This conversion will take place only if A is a subclass of LabelledFormula (A <: LabelledFormula).
    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:
    (sequent: Sequent[Formula]).indexOfPolOption(elem, pol)
    Annotations
    @deprecated
    Deprecated

    (Since version 2.9) Use indexOfOption instead.

  6. def indexOfPolOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
    Annotations
    @deprecated
    Deprecated

    (Since version 2.9) Use indexOfOption instead.

  7. def →[B](y: B): (Sequent[A], B)
    Implicit
    This member is added by an implicit conversion from Sequent[A] toArrowAssoc[Sequent[A]] performed by method ArrowAssoc in scala.Predef.This conversion will take place only if A is a subclass of LabelledFormula with FOLFormula (A <: LabelledFormula with FOLFormula).
    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.

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion RichClause fromSequent[A] to RichClause[A]

Inherited by implicit conversion RichFOLSequent fromSequent[A] to RichFOLSequent

Inherited by implicit conversion RichFormulaSequent fromSequent[A] to RichFormulaSequent

Inherited by implicit conversion labelledSequentToSequent fromSequent[A] to Sequent[Formula]

Inherited by implicit conversion any2stringadd fromSequent[A] to any2stringadd[Sequent[A]]

Inherited by implicit conversion StringFormat fromSequent[A] to StringFormat[Sequent[A]]

Inherited by implicit conversion Ensuring fromSequent[A] to Ensuring[Sequent[A]]

Inherited by implicit conversion ArrowAssoc fromSequent[A] to ArrowAssoc[Sequent[A]]

Ungrouped