Packages

case class TermState(terms: FiniteDistribution[Term], typs: FiniteDistribution[Typ[Term]], vars: Vector[Term] = Vector(), inds: FiniteDistribution[ExstInducDefn] = FD.empty[ExstInducDefn], goals: FiniteDistribution[Typ[Term]] = FD.empty, context: Context = Context.Empty) extends TermsTypThms with Product with Serializable

A state, typically the initial state, for generating terms, types etc

terms

distribution of terms

typs

distribution of types

vars

variables, over which we may take closures

inds

inductive type definitions

Linear Supertypes
Serializable, Product, Equals, TermsTypThms, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TermState
  2. Serializable
  3. Product
  4. Equals
  5. TermsTypThms
  6. AnyRef
  7. 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 TermState(terms: FiniteDistribution[Term], typs: FiniteDistribution[Typ[Term]], vars: Vector[Term] = Vector(), inds: FiniteDistribution[ExstInducDefn] = FD.empty[ExstInducDefn], goals: FiniteDistribution[Typ[Term]] = FD.empty, context: Context = Context.Empty)

    terms

    distribution of terms

    typs

    distribution of types

    vars

    variables, over which we may take closures

    inds

    inductive type definitions

Value Members

  1. def ++(that: TermState): TermState
  2. def addTerm(x: Term, varWeight: Double = 0.3): (TermState, Term)
  3. def addVar(typ: Typ[Term], varWeight: Double): (TermState, Term)
  4. lazy val allTyps: Set[Typ[Term]]
  5. lazy val bestProofs: Map[Typ[Term], Term]
  6. val context: Context
    Definition Classes
    TermState → TermsTypThms
  7. def contextExport(ctx: Context = context): TermState
  8. def contextImport(ctx: Context): TermState
  9. def contextInit(ctx: Context, varWeight: Double): TermState
  10. lazy val contradicted: Vector[(Typ[Term], Double, FiniteDistribution[Term])]
  11. def distTangent(fd: FiniteDistribution[Term]): TermState
  12. def export(variables: Vector[Term]): TermState
  13. lazy val extraTyps: Set[Typ[U] forSome {type U >: x$17.type <: Term with Subs[U], val x$17: Term}]
  14. lazy val fullPfSet: Vector[(Term, Term)]
  15. lazy val funcDist: FiniteDistribution[ExstFunc]
  16. lazy val funcsWithDoms: Map[Typ[Term], FiniteDistribution[ExstFunc]]
  17. lazy val goalSet: Set[Typ[Term]]
    Definition Classes
    TermsTypThms
  18. def goalThmsBySt(goalW: Double): FiniteDistribution[Typ[Term]]
    Definition Classes
    TermsTypThms
  19. val goals: FiniteDistribution[Typ[Term]]
    Definition Classes
    TermState → TermsTypThms
  20. def inIsle(x: Term): TermState
  21. val inds: FiniteDistribution[ExstInducDefn]
    Definition Classes
    TermState → TermsTypThms
  22. def isProd(typ: Typ[Term]): Boolean
  23. def json: Obj
    Definition Classes
    TermsTypThms
  24. lazy val lemmas: Vector[(Typ[Term], Option[Term], Double)]
  25. lazy val orderedUnknowns: Vector[Typ[Term]]
  26. lazy val pfDist: FiniteDistribution[Term]
  27. lazy val pfMap: Map[Typ[Term], Vector[Term]]
  28. lazy val pfSet: Vector[Term]
  29. def productElementNames: Iterator[String]
    Definition Classes
    Product
  30. def purge(epsilon: Double): TermState
  31. lazy val remainingGoals: FiniteDistribution[Typ[Term]]
  32. def subGoalsFromFunc(f: Term): FiniteDistribution[Typ[Term]]
  33. def subs(x: Term, y: Term): TermState
  34. lazy val successTerms: Set[Term]
  35. lazy val successes: Vector[(Typ[Term], Double, Term)]
  36. def tangent(xs: Term*): TermState
    Definition Classes
    TermState → TermsTypThms
  37. lazy val termSet: Set[Term]
    Definition Classes
    TermsTypThms
  38. lazy val termTyps: Set[Typ[Term]]
  39. lazy val termTypsSet: Set[Typ[U] forSome {type U >: x$1.type <: Term with Subs[U], val x$1: Term}]
    Definition Classes
    TermsTypThms
  40. lazy val termWithTyps: Map[Typ[Term], FiniteDistribution[Term]]
  41. val terms: FiniteDistribution[Term]
    Definition Classes
    TermState → TermsTypThms
  42. lazy val thmWeights: Vector[(Typ[Term], Double, Double, Double)]
    Definition Classes
    TermsTypThms
  43. lazy val thmsByPf: FiniteDistribution[Typ[Term]]
    Definition Classes
    TermsTypThms
  44. lazy val thmsByPfMap: Map[Typ[Term], Double]
  45. lazy val thmsBySt: FiniteDistribution[Typ[Term]]
    Definition Classes
    TermsTypThms
  46. lazy val thmsByStMap: Map[Typ[Term], Double]
  47. lazy val typFamilyDist: FiniteDistribution[ExstFunc]
  48. lazy val typOrFamilyDist: FiniteDistribution[Term]
  49. lazy val typOrFamilyDistMap: Map[Term, Double]
  50. lazy val typSet: Set[Typ[Term]]
    Definition Classes
    TermsTypThms
  51. val typs: FiniteDistribution[Typ[Term]]
    Definition Classes
    TermState → TermsTypThms
  52. lazy val unknownStatements: FiniteDistribution[Typ[Term]]
  53. val vars: Vector[Term]
    Definition Classes
    TermState → TermsTypThms
  54. def withTyps(fd: FiniteDistribution[Typ[Term]]): TermState