Packages

c

provingground.learning.HoTTMessages

IntermediateStatements

case class IntermediateStatements(typ: Typ[Term], lemmas: FiniteDistribution[Typ[Term]]) extends Product with Serializable

Given a type, a lemma is the type of an ingredient of the generating set, ideally not easily inhabited. These are candidate lemmas

typ

the goal

lemmas

candidate lemmas

Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IntermediateStatements
  2. Serializable
  3. Product
  4. Equals
  5. AnyRef
  6. 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

Instance Constructors

  1. new IntermediateStatements(typ: Typ[Term], lemmas: FiniteDistribution[Typ[Term]])

    typ

    the goal

    lemmas

    candidate lemmas

Value Members

  1. val lemmas: FiniteDistribution[Typ[Term]]
  2. def productElementNames: Iterator[String]
    Definition Classes
    Product
  3. val typ: Typ[Term]