case class NDSequent[+A](assumptions: Seq[A], conclusion: A) extends Product with Serializable
Sequents for natural deduction.
They have the form A1,...,Am :- B (there is always exactly one element in the succedent).
- A
The type of elements in the sequent.
- assumptions
The elements A1,...,Am.
- conclusion
The element B.
- Source
- NDSequent.scala
Linear Supertypes
Type Hierarchy
Ordering
- Alphabetic
- By Inheritance
Inherited
- NDSequent
- Serializable
- Product
- Equals
- AnyRef
- Any
Implicitly
- by toSequent
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
Visibility
- Public
- Protected
Instance Constructors
- new NDSequent(assumptions: Seq[A], conclusion: A)
- assumptions
The elements A1,...,Am.
- conclusion
The element B.
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ++[B >: A](that: Sequent[B]): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def ++:[B >: A](additionalAssumptions: Iterable[B]): NDSequent[B]
- def +:[B >: A](additionalAssumption: B): NDSequent[B]
- def ->[B](y: B): (NDSequent[A], B)
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def :-[B >: A](newConclusion: B): NDSequent[B]
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val antecedent: Vector[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def apply(is: Seq[SequentIndex]): Seq[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val assumptions: Seq[A]
- def cedent(polarity: Polarity): Vector[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- def collect[B](f: PartialFunction[A, B]): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- val conclusion: A
- def contains[B](el: B, polarity: Polarity): Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def delete(is: SequentIndex*)(implicit d: DummyImplicit): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def delete(is: Seq[SequentIndex]): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def delete(i: SequentIndex): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def distinct: Sequent[A]
Removes duplicate formulas from both cedents.
Removes duplicate formulas from both cedents.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def elements: Vector[A]
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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def ensuring(cond: (NDSequent[A]) => Boolean, msg: => Any): NDSequent[A]
- def ensuring(cond: (NDSequent[A]) => Boolean): NDSequent[A]
- def ensuring(cond: Boolean, msg: => Any): NDSequent[A]
- def ensuring(cond: Boolean): NDSequent[A]
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def exists(p: (A) => Boolean): Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def find(pred: (A) => Boolean): Option[SequentIndex]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def flatMap[B](f: (A) => IterableOnce[B], g: (A) => IterableOnce[B]): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def flatMap[B](f: (A) => IterableOnce[B]): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def forall(p: (A) => Boolean): Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def foreach[U](f: (A) => U): Unit
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- def groupBy[B](f: (A) => B): Sequent[(B, Vector[A])]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOf[B >: A](elem: B, polarity: Polarity): SequentIndex
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOf[B >: A](elem: B): SequentIndex
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOfInAnt[B >: A](elem: B): SequentIndex
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOfInSuc[B >: A](elem: B): SequentIndex
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOfOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indexOfOption[B >: A](elem: B): Option[SequentIndex]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def indicesWherePol(p: (A) => Boolean, pol: Polarity): Vector[SequentIndex]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def insertAt[B >: A](i: SequentIndex, el: B): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def intersect[B >: A](other: Sequent[B]): Sequent[A]
Computes the intersection of two sequents.
Computes the intersection of two sequents.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isSubMultisetOf[B >: A](other: Sequent[B]): Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def isTaut: Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def nonEmpty: Boolean
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- def polarizedElements: Vector[(A, 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def removeFromAntecedent[B](e: B): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def removeFromSuccedent[B](e: B): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def replaceAt[B >: A](i: SequentIndex, el: B): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def size: Int
Synonym for length.
Synonym for length.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def sizes: (Int, Int)
Synonym for lengths.
Synonym for lengths.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def sortBy[B](f: (A) => B)(implicit ord: Ordering[B]): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def sorted[B >: A](implicit ordering: Ordering[B]): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- val succedent: Vector[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def swapped: Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def tautFormula: Option[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def tautFormulas: Vector[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def toSigRelativeString(implicit sig: BabelSignature): String
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def toString(): String
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent → AnyRef → Any
- def toTuple: (Vector[A], Vector[A])
- returns
The sequent in tuple form.
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def updated[B >: A](updates: Iterable[(SequentIndex, B)]): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def updated[B >: A](index: SequentIndex, elem: B): Sequent[B]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- 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])
- def withFilter(p: (A) => Boolean): Sequent[A]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def zip[B](that: Sequent[B]): Sequent[(A, B)]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- def zipWithIndex: Sequent[(A, SequentIndex)]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
Shadowed Implicit Value Members
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- 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:(nDSequent: Sequent[A]).++:(es)
- Definition Classes
- Sequent
- 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 NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- 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:(nDSequent: Sequent[A]).+:(e)
- Definition Classes
- Sequent
- def productElementNames: Iterator[String]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- 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:(nDSequent: Sequent[A]).productElementNames
- Definition Classes
- Product
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 NDSequent[A] toStringFormat[NDSequent[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 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 indexOfPol[B >: A](elem: B, polarity: Polarity): SequentIndex
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- Annotations
- @deprecated
- Deprecated
(Since version 2.9) Use indexOf instead.
- def indexOfPolOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toSequent[A] performed by method toSequent in gapt.proofs.NDSequent.
- Definition Classes
- Sequent
- Annotations
- @deprecated
- Deprecated
(Since version 2.9) Use indexOfOption instead.
- def →[B](y: B): (NDSequent[A], B)
- Implicit
- This member is added by an implicit conversion from NDSequent[A] toArrowAssoc[NDSequent[A]] 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.