Packages

o

provingground.learning

StrategicProvers

object StrategicProvers

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. StrategicProvers
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type SeekResult = (Successes, Set[EquationNode], Set[Term])
  2. type Successes = Vector[(Typ[Term], Double, Term)]

Value Members

  1. def concurrentTargetChomper(lp: LocalProver, typGroups: Vector[Vector[Typ[Term]]], concurrency: Int = Utils.threadNum, accumSucc: Successes = Vector(), accumFail: Vector[Typ[Term]] = Vector(), accumEqs: Set[EquationNode] = Set(), accumTerms: Set[Term] = Set()): Task[(Successes, Vector[Typ[Term]], Set[EquationNode], Set[Term])]
  2. var currentGoal: Option[Typ[Term]]
  3. var equationNodes: Set[EquationNode]
  4. val failures: ArrayBuffer[Typ[Term]]
  5. def formal(sc: Successes): Set[EquationNode]
  6. def goalChomper(lp: LocalProver, typs: Vector[Typ[Term]], accumSucc: Successes = Vector(), accumEqs: Set[EquationNode] = Set(), accumTerms: Set[Term] = Set(), scale: Double = 2, maxSteps: Int = 100): Task[(Successes, Set[EquationNode], Set[Term], Vector[Typ[Term]])]
  7. def liberalChomper(lp: LocalProver, typs: Vector[Typ[Term]], accumSucc: Successes = Vector(), accumFail: Vector[Typ[Term]] = Vector(), accumEqs: Set[EquationNode] = Set(), accumTerms: Set[Term] = Set(), scale: Double = 2, maxSteps: Int = 100): Task[(Successes, Vector[Typ[Term]], Set[EquationNode], Set[Term])]
  8. def md: String
  9. def seekGoal(lp: LocalProver, typ: Typ[Term], terms: Set[Term], scale: Double = 2, maxSteps: Int = 100): Task[SeekResult]
  10. def seekTyp(lp: LocalProver, typ: Typ[Term], terms: Set[Term]): Task[SeekResult]
  11. def solveTyp(lp: LocalProver, typ: Typ[Term], terms: Set[Term]): Task[SeekResult]
  12. val successes: ArrayBuffer[Successes]
  13. def targetChomper(lp: LocalProver, typs: Vector[Typ[Term]], accumSucc: Successes = Vector(), accumFail: Vector[Typ[Term]] = Vector(), accumEqs: Set[EquationNode] = Set(), accumTerms: Set[Term] = Set()): Task[(Successes, Vector[Typ[Term]], Set[EquationNode], Set[Term])]
  14. var termSet: Set[Term]
  15. var update: (Unit) => Unit
  16. object SeekResult