Type Members

1.  case class AddVariable(typ: Typ[Term]) extends Product with Serializable
2.  case class BaseMixinLemmas(lemmas: ParVector[(Typ[Term], Option[Term], Double)]) extends Product with Serializable
3.  case class ChompResult(successes: Successes, failures: Vector[Typ[Term]], eqns: Set[EquationNode]) extends Product with Serializable

   result of goal chomping

   result of goal chomping

   successes

   results proved

   failures

   results neither proved nor disproved

   eqns

   equations contributed as a by-product

4.  case class Consequence(premise: Typ[Term], conclusion: Typ[Term], proofMapOpt: Option[ExstFunc], context: Context) extends PropagateProof with Product with Serializable
5.  case class ConsiderInductiveTypes(inducs: FiniteDistribution[ExstInducDefn]) extends Product with Serializable

   introduce inductive types

   introduce inductive types

   inducs

   distribution on inductive types introduced

6.  case class ConsiderTerms(terms: FiniteDistribution[Term]) extends Product with Serializable

   terms to use for proving, possibly the axioms etc not used in generating types.

   terms to use for proving, possibly the axioms etc not used in generating types.

   terms

   the term distribution to use

7.  case class Contradicted(statement: Typ[Term], contraOpt: Option[ExstFunc], context: Context) extends Decided with Product with Serializable
8.  case class Contradicts(premise: Typ[Term], conclusion: Typ[Term], contraMapOpt: Option[ExstFunc], context: Context) extends PropagateProof with Product with Serializable
9.  sealed trait Decided extends AnyRef
10.  case class FailedToProve(statement: Typ[Term], context: Context, forConsequences: Vector[Typ[Term]] = Vector()) extends Product with Serializable
11.  case class FinalState(ts: TermState) extends Product with Serializable

    result of evolution, say of a local-prover; could be just from equations

    result of evolution, say of a local-prover; could be just from equations

    ts

    the evolved state

12.  case class FromAll(typs: Vector[Typ[Term]], conclusion: Typ[Term], proofOpt: Option[Term], context: Context, forConsequences: Vector[Typ[Term]]) extends PropagateProof with Product with Serializable
13.  case class FromAny(typs: Vector[Typ[Term]], conclusion: Typ[Term], exhaustive: Boolean, proofsOpt: Vector[Option[ExstFunc]], context: Context, forConsequences: Vector[Typ[Term]]) extends PropagateProof with Product with Serializable
14.  case class FunctionForGoal(fn: Term, goal: Typ[Term], context: Context, forConsequences: Vector[Typ[Term]] = Vector()) extends Product with Serializable
15.  case class GeneratedEquationNodes(eqn: Set[EquationNode], preNormalized: Boolean = false) extends Product with Serializable

    Result of generation and normalization

    Result of generation and normalization

    eqn

    resulting equation nodes to use

16.  case class HaltIf(condition: (Unit) => Boolean) extends Product with Serializable
17.  case class InitState(ts: TermState, weight: Double) extends Product with Serializable

    an initial term state from which to evolve, perhaps just to generate types

    an initial term state from which to evolve, perhaps just to generate types

    ts

    the term-state

18.  case class Instance(term: Term, typ: Typ[Term], context: Context) extends Product with Serializable

    instances, which are just terms of a specific type in a context

    instances, which are just terms of a specific type in a context

    term

    the instance term

    typ

    the goal type

    context

    the context

19.  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.

    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

20.  case class Lemmas(lemmas: ParVector[(Typ[Term], Option[Term], Double)], byStatement: Option[Map[Typ[Term], Double]] = None) extends Product with Serializable

    lemmas that have been identified based on non-triviality (and possibly goals) from a final state.

    lemmas that have been identified based on non-triviality (and possibly goals) from a final state.

    lemmas

    the lemmas with weights

21.  class ModifyParams extends AnyRef

    modifying parameters, for instance excluding islands, strengthening backward reasoning etc for serialization, inherit from this class

22.  case class NarrowOptimizeGenerators(pow: Double, hW: Double, klW: Double, smoothing: Double, decay: Double) extends Product with Serializable
23.  case class OptimalInitial(lp: LocalProver, hW: Double, klW: Double, smoothing: Double, decay: Double) extends Product with Serializable
24.  case class OptimizeGenerators(decay: Double) extends Product with Serializable
25.  case class ProofLambda(outerGoal: Typ[Term], innerGoal: Typ[Term], outerContext: Context, innerContext: Context, variable: Term, isDependent: Boolean) extends Product with Serializable
26.  trait PropagateProof extends AnyRef
27.  case class Proved(statement: Typ[Term], proofOpt: Option[Term], context: Context) extends Decided with Product with Serializable
28.  trait ReasonBackward extends AnyRef

    instruction to generate subgoals from a given goal, using a function with eventual codomain, induction etc

29.  case class RelatedStatements(typ: Typ[Term], related: FiniteDistribution[Typ[Term]]) extends Product with Serializable

    Other types that are likely to have common ingredients in proofs

    Other types that are likely to have common ingredients in proofs

    typ

    the original type

    related

    types related

30.  case class RepresentationMap(rep: Map[Variable[_], Vector[Double]]) extends Product with Serializable
31.  case class ResolveGoal(goal: Typ[Term]) extends ReasonBackward with Product with Serializable

    backward reasoning for special types - products, co-products, Sigma-types and Pi-types; respond with seeking instantiations and adding variables for the last two cases.

    backward reasoning for special types - products, co-products, Sigma-types and Pi-types; respond with seeking instantiations and adding variables for the last two cases.

    goal

    type to resolve

32.  case class SeekEventualCodomain(goal: Typ[Term]) extends ReasonBackward with Product with Serializable
33.  case class SeekGoal(goal: Typ[Term], context: Context, forConsequences: Vector[Typ[Term]] = Vector()) extends Product with Serializable

    A goal to seek, often derived from others; if the others are solved or negated, we stop seeking

    A goal to seek, often derived from others; if the others are solved or negated, we stop seeking

    goal

    the goal

    forConsequences

    the consequences for which we seek this, if any; if empty these have no effect

34.  case class SeekGoals(goals: FiniteDistribution[Typ[Term]], context: Context) extends Product with Serializable

    goals to seek, through whatever means,

    goals to seek, through whatever means,

    goals

    the goals

35.  case class SeekInduction(goal: Typ[Term]) extends ReasonBackward with Product with Serializable
36.  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

37.  case class SeekLemmas(weightPower: Double, scale: Double) extends Product with Serializable

    instruction to seek lemmas

    instruction to seek lemmas

    weightPower

    power to flatten distributions

    scale

    scale?

38.  case class SpecialInitState(ts: TermState, baseCutoff: Double = math.pow(10, -4), lemmaMix: Double = 0.5, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None) extends Product with Serializable
39.  case class SplitFocus(number: Int, scale: Double) extends Product with Serializable
40.  case class TangentBaseState(ts: TermState, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None, evOpt: Option[ExpressionEquationSolver] = None, initOpt: Option[SpecialInitState] = None) extends Product with Serializable
41.  case class TangentLemmas(lemmas: ParVector[(Typ[Term], Option[Term], Double)]) extends Product with Serializable
42.  case class TangentWithTerm(term: Term, weight: Double) extends Product with Serializable

    proceed by tangent evolution, perhaps from a lemma

    proceed by tangent evolution, perhaps from a lemma

    term

    tangent direction

    weight

    weight

43.  case class TautologyInitState(tautGen: TermState) extends Product with Serializable
44.  case class TimeLimit(duration: FiniteDuration) extends Product with Serializable
45.  case class UseLemma(lemma: Typ[Term], proofOpt: Option[Term]) extends Product with Serializable

    instruction to use a lemma - could be as a tangent or mixing in to generators if mixing in just call ConsiderTerms

    instruction to use a lemma - could be as a tangent or mixing in to generators if mixing in just call ConsiderTerms

    lemma

    lemma statement

46.  case class UseLemmaDistribution(lemmas: FiniteDistribution[Typ[Term]], proofOptMap: Option[Map[Typ[Term], Term]]) extends Product with Serializable

    instruction to use a distribution of lemmas - could be as a tangent or mixing in to generators if mixing in just call ConsiderTerms

    instruction to use a distribution of lemmas - could be as a tangent or mixing in to generators if mixing in just call ConsiderTerms

    lemmas

    statement of lemmas

    proofOptMap

    optional proofs

47.  case class UsedLemmas(lemmas: ParVector[(Typ[Term], Double)]) extends Product with Serializable
48.  case class Weight(scale: Double) extends Product with Serializable
49.  type WithWeight[A] = ::[Weight, ::[A, HNil]]