case class BindingContext extends PartialOrdering[ConstantTerm] with Product with Serializable
Class to represent the context of constants bound above a certain node in the proof tree. This constant can be seen as a partial ordering on constants: inner bound constants are bigger than outer bound constants
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- BindingContext
- Product
- Equals
- PartialOrdering
- Equiv
- Serializable
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def addAndContract(c: Iterable[ConstantTerm], q: Quantifier): BindingContext
Add new innermost bound constants to the binding context.
Add new innermost bound constants to the binding context. If the quantifier of the new constants is the same as of the innermost constant group, just add the constants to the group
- def addAndContract(c: ConstantTerm, q: Quantifier): BindingContext
Add a new innermost bound constant to the binding context.
Add a new innermost bound constant to the binding context. If the quantifier of the new constant is the same as of the innermost constant group, just add the constant to the group
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def binder(c: ConstantTerm): Option[Quantifier]
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- val constantSeq: List[(Quantifier, Set[ConstantTerm])]
- def containsMaximumConstantWith(consts: Iterable[ConstantTerm], p: (ConstantTerm) => Boolean): Boolean
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equiv(x: ConstantTerm, y: ConstantTerm): Boolean
- Definition Classes
- PartialOrdering → Equiv
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def gt(x: ConstantTerm, y: ConstantTerm): Boolean
- Definition Classes
- PartialOrdering
- def gteq(x: ConstantTerm, y: ConstantTerm): Boolean
- Definition Classes
- PartialOrdering
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def lt(x: ConstantTerm, y: ConstantTerm): Boolean
- Definition Classes
- PartialOrdering
- def lteq(x: ConstantTerm, y: ConstantTerm): Boolean
- Definition Classes
- BindingContext → PartialOrdering
- def maximumConstants(consts: Iterable[ConstantTerm]): Seq[ConstantTerm]
Filter out and return the maximum elements of a given collection of constants
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def reverse: PartialOrdering[ConstantTerm]
- Definition Classes
- PartialOrdering
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def tryCompare(x: ConstantTerm, y: ConstantTerm): Option[Int]
- Definition Classes
- BindingContext → PartialOrdering
- 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])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)