Packages

trait SeekInstances extends AnyRef

Instances to be found for a goal which is a sigma-type corresponding to an instance we get a new goal, and that the original is a consequnce of the new goal

Linear Supertypes
AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SeekInstances
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. abstract type U <: Term with Subs[U]
  2. abstract type V <: Term with Subs[V]

Abstract Value Members

  1. abstract val context: Context
  2. abstract val forConsequences: Vector[Typ[Term]]
  3. abstract val goal: TypFamily[U, V]
  4. abstract val typ: Typ[U]

Concrete Value Members

  1. def goalCast(t: Term): Typ[V]
  2. def sigma: SigmaTyp[U, V]
  3. def toString(): String
    Definition Classes
    SeekInstances → AnyRef → Any