gapt
2.19.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/NDSequent

NDSequent

gapt.proofs.NDSequent
See theNDSequent companion object
case class NDSequent[+A](assumptions: Seq[A], conclusion: A)

Sequents for natural deduction.

They have the form A,,1,,,...,A,,m,, :- B (there is always exactly one element in the succedent).

Type parameters

A

The type of elements in the sequent.

Value parameters

assumptions

The elements A,,1,,,...,A,,m,,.

conclusion

The element B.

Attributes

Companion
object
Source
NDSequent.scala
Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all

Members list

Value members

Concrete methods

def ++[B >: A](that: Sequent[B]): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def ++:[B >: A](es: Iterable[B]): Sequent[B]
Implicitly added by toSequent

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

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

Value parameters

es

A collection of elements of type B > A.

Attributes

Returns

The sequent with es added to the antecedent.

Source
sequents.scala
def ++:[B >: A](additionalAssumptions: Iterable[B]): NDSequent[B]

Attributes

Source
NDSequent.scala
def +:[B >: A](e: B): Sequent[B]
Implicitly added by toSequent

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

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

Value parameters

e

An element of type B > A

Attributes

Returns

The sequent with e added to the antecedent

Source
sequents.scala
def +:[B >: A](additionalAssumption: B): NDSequent[B]

Attributes

Source
NDSequent.scala
def :+[B >: A](e: B): Sequent[B]
Implicitly added by toSequent

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

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

Value parameters

e

An element of type B > A

Attributes

Returns

The sequent with e added to the succedent

Source
sequents.scala
def :++[B >: A](es: Iterable[B]): Sequent[B]
Implicitly added by toSequent

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

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

Value parameters

es

A collection of elements of type B > A.

Attributes

Returns

The sequent with es added to the succedent.

Source
sequents.scala
def :-[B >: A](newConclusion: B): NDSequent[B]

Attributes

Source
NDSequent.scala
def apply(i: SequentIndex): A
Implicitly added by toSequent

Returns the element at some SequentIndex.

Returns the element at some SequentIndex.

Value parameters

i

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

Attributes

Returns

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

Source
sequents.scala
def apply(is: Seq[SequentIndex]): Seq[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def cedent(polarity: Polarity): Vector[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def collect[B](f: PartialFunction[A, B]): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def contains[B](el: B): Boolean
Implicitly added by toSequent

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

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

Attributes

Source
sequents.scala
def contains[B](el: B, polarity: Polarity): Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def delete(i: SequentIndex): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def delete(is: Seq[SequentIndex]): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def delete(is: SequentIndex*)(implicit d: DummyImplicit): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def diff[B >: A](other: Sequent[B]): Sequent[A]
Implicitly added by toSequent

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

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

Attributes

Source
sequents.scala
def distinct: Sequent[A]
Implicitly added by toSequent

Removes duplicate formulas from both cedents.

Removes duplicate formulas from both cedents.

Attributes

Source
sequents.scala
def elements: Vector[A]
Implicitly added by toSequent

Sequence of elements of the sequent.

Sequence of elements of the sequent.

Attributes

Returns

Antecedent concatenated with succedent.

Source
sequents.scala
def exists(p: A => Boolean): Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def filter(p: A => Boolean): Sequent[A]
Implicitly added by toSequent

The sub-sequent of elements satisfying some predicate.

The sub-sequent of elements satisfying some predicate.

Value parameters

p

A function of type A => Boolean.

Attributes

Returns

The sequent consisting of only those elements satisfying p.

Source
sequents.scala
def filterNot(p: A => Boolean): Sequent[A]
Implicitly added by toSequent

The sub-sequent of elements not satisfying some predicate.

The sub-sequent of elements not satisfying some predicate.

Value parameters

p

A function of type A => Boolean.

Attributes

Returns

The sequent consisting of only those elements not satisfying p.

Source
sequents.scala
def find(pred: A => Boolean): Option[SequentIndex]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def flatMap[B](f: A => IterableOnce[B]): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def flatMap[B](f: A => IterableOnce[B], g: A => IterableOnce[B]): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def focus(i: SequentIndex): (A, Sequent[A])
Implicitly added by toSequent

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

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

Value parameters

i

A SequentIndex.

Attributes

Returns

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

Source
sequents.scala
def forall(p: A => Boolean): Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def foreach[U](f: A => U): Unit
Implicitly added by toSequent

Attributes

Source
sequents.scala
def groupBy[B](f: A => B): Sequent[(B, Vector[A])]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOf[B >: A](elem: B): SequentIndex
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOf[B >: A](elem: B, polarity: Polarity): SequentIndex
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOfInAnt[B >: A](elem: B): SequentIndex
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOfInSuc[B >: A](elem: B): SequentIndex
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOfOption[B >: A](elem: B): Option[SequentIndex]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indexOfOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def indices: Vector[SequentIndex]
Implicitly added by toSequent

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

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

Attributes

Source
sequents.scala
def indicesSequent: Sequent[SequentIndex]
Implicitly added by toSequent

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

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

Attributes

Source
sequents.scala
def indicesWhere(p: A => Boolean): Vector[SequentIndex]
Implicitly added by toSequent

Returns the list of indices of elements satisfying some predicate.

Returns the list of indices of elements satisfying some predicate.

Value parameters

p

A function of type A => Boolean.

Attributes

Source
sequents.scala
def indicesWherePol(p: A => Boolean, pol: Polarity): Vector[SequentIndex]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def insertAt[B >: A](i: SequentIndex, el: B): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def intersect[B >: A](other: Sequent[B]): Sequent[A]
Implicitly added by toSequent

Computes the intersection of two sequents.

Computes the intersection of two sequents.

Attributes

Source
sequents.scala
def isDefinedAt(i: SequentIndex): Boolean
Implicitly added by toSequent

Tests whether the sequent is defined at the supplied SequentIndex.

Tests whether the sequent is defined at the supplied SequentIndex.

Attributes

Source
sequents.scala
def isEmpty: Boolean
Implicitly added by toSequent

Returns true iff both cedents are empty.

Returns true iff both cedents are empty.

Attributes

Source
sequents.scala
def isSubMultisetOf[B >: A](other: Sequent[B]): Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def isSubsetOf[B >: A](other: Sequent[B]): Boolean
Implicitly added by toSequent

Value parameters

other

Another Sequent.

Attributes

Returns

True iff other contains this pair of sets.

Source
sequents.scala
def isTaut: Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def length: Int
Implicitly added by toSequent

The number of elements in the sequent.

The number of elements in the sequent.

Attributes

Source
sequents.scala
def lengths: (Int, Int)
Implicitly added by toSequent

A pair consisting of the lengths of the cedents.

A pair consisting of the lengths of the cedents.

Attributes

Source
sequents.scala
def map[B](f: A => B): Sequent[B]
Implicitly added by toSequent

Maps a function over both cedents

Maps a function over both cedents

Type parameters

B

The return type of f

Value parameters

f

A function of type A => B

Attributes

Returns

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

Source
sequents.scala
def map[B](f: A => B, g: A => B): Sequent[B]
Implicitly added by toSequent

Maps two functions over the antecedent and succedent, respectively.

Maps two functions over the antecedent and succedent, respectively.

Type parameters

B

The return type of f and g.

Value parameters

f

The function to map over the antecedent.

g

The function to map over the succedent.

Attributes

Returns

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

Source
sequents.scala
def multiSetEquals[B](other: Sequent[B]): Boolean
Implicitly added by toSequent

Equality treating each side of the sequent as a multiset.

Equality treating each side of the sequent as a multiset.

Attributes

Source
sequents.scala
def nonEmpty: Boolean
Implicitly added by toSequent

Attributes

Source
sequents.scala
def polarizedElements: Vector[(A, Polarity)]
Implicitly added by toSequent

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.

Attributes

Source
sequents.scala
def removeFromAntecedent[B](e: B): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def removeFromSuccedent[B](e: B): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def replaceAt[B >: A](i: SequentIndex, el: B): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def setEquals[B](other: Sequent[B]): Boolean
Implicitly added by toSequent

Equality treating each side of the sequent as a set.

Equality treating each side of the sequent as a set.

Attributes

Source
sequents.scala
def size: Int
Implicitly added by toSequent

Synonym for length.

Synonym for length.

Attributes

Source
sequents.scala
def sizes: (Int, Int)
Implicitly added by toSequent

Synonym for lengths.

Synonym for lengths.

Attributes

Source
sequents.scala
def sortBy[B](f: A => B)(implicit ord: Ordering[B]): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def sorted[B >: A](implicit ordering: Ordering[B]): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def swapped: Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def tautFormula: Option[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def tautFormulas: Vector[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def toSigRelativeString(implicit sig: BabelSignature): String
Implicitly added by toSequent

Attributes

Source
sequents.scala
def toTuple: (Vector[A], Vector[A])
Implicitly added by toSequent

Attributes

Returns

The sequent in tuple form.

Source
sequents.scala
def updated[B >: A](index: SequentIndex, elem: B): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def updated[B >: A](updates: Iterable[(SequentIndex, B)]): Sequent[B]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def withFilter(p: A => Boolean): Sequent[A]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def zip[B](that: Sequent[B]): Sequent[(A, B)]
Implicitly added by toSequent

Attributes

Source
sequents.scala
def zipWithIndex: Sequent[(A, SequentIndex)]
Implicitly added by toSequent

Attributes

Source
sequents.scala

Deprecated methods

def indexOfPol[B >: A](elem: B, polarity: Polarity): SequentIndex
Implicitly added by toSequent

Attributes

Deprecated
[Since version 2.9]
Source
sequents.scala
def indexOfPolOption[B >: A](elem: B, pol: Polarity): Option[SequentIndex]
Implicitly added by toSequent

Attributes

Deprecated
[Since version 2.9]
Source
sequents.scala

Inherited methods

def productElementNames: Iterator[String]
Implicitly added by toSequent

Attributes

Inherited from:
Product
def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]
Implicitly added by toSequent

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product
Generated with