Packages

object LeanToTermMonix extends Serializable

Annotations
@deprecated
Deprecated

(Since version buggy, avoid) use LeanParser

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

Type Members

  1. type TaskParser = (Expr, Vector[Term]) => Task[Term]

Value Members

  1. def addChunk(mods: Vector[Modification], init: Task[LeanToTermMonix] = Task.eval(empty), limit: FiniteDuration = 3.minutes): Task[LeanToTermMonix]
  2. val applWork: Set[(Term, Term)]
  3. def applyFuncOptWitFold(ft: Task[Option[Term]], v: Vector[Option[Term]]): Task[Option[Term]]
  4. def applyFuncWit(f: Term, x: Term): Term
  5. def applyFuncWitFold(ft: Task[Term], v: Vector[Term]): Task[Term]
  6. def applyFuncWitOpt(f: Term, x: Term): Option[Term]
  7. def applyOptFuncWit(fo: Option[Term], xo: Option[Term]): Option[Term]
  8. def applyWitUnify(f: Term, x: Term): Option[Term]
  9. var arg: Term
  10. def defFromMod(name: Name, ltm: LeanToTermMonix, mods: Vector[Modification]): Option[Task[(Term, LeanToTermMonix)]]
  11. val empty: LeanToTermMonix
  12. def feedWit(t: Term): Option[Term]
  13. def findMod(name: Name, mods: Vector[Modification]): Option[Modification]
  14. def foldAxiomSeq(accum: Vector[Term], axs: Vector[(Name, Expr)], ltmT: Task[LeanToTermMonix], mods: Vector[Modification]): Task[(Vector[Term], LeanToTermMonix)]
  15. def fromMods(mods: Vector[Modification], init: LeanToTermMonix = empty): Task[LeanToTermMonix]
  16. var func: Term
  17. def getValue(t: Term, n: Int, accum: Vector[Term]): Task[(Term, Vector[Term])]
  18. def indModFromMod(name: Name, ltm: LeanToTermMonix, mods: Vector[Modification]): Option[Task[(TermIndMod, LeanToTermMonix)]]
  19. def iterant(mods: Vector[Modification], init: LeanToTermMonix = empty, limit: FiniteDuration = 5.minutes, logErr: (Modification, Throwable) => Unit = (_, _) => {}, recoverAll: Boolean = true): Iterant[Task, LeanToTermMonix]
  20. def modNames(mod: Modification): Vector[Name]
  21. def observable(mods: Vector[Modification], init: LeanToTermMonix = empty, limit: FiniteDuration = 5.minutes, logErr: (Modification, Throwable) => Unit = (_, _) => {}): Observable[LeanToTermMonix]
  22. def parse(exp: Expr, vars: Vector[Term], ltm: LeanToTermMonix, mods: Vector[Modification]): Task[(Term, LeanToTermMonix)]
  23. def parseVec(vec: Vector[Expr], vars: Vector[Term], ltm: LeanToTermMonix, mods: Vector[Modification]): Task[(Vector[Term], LeanToTermMonix)]
  24. def witUnify(x: Term, typ: Typ[Term]): Option[Term]
  25. def withAxiom(name: Name, ty: Expr, ltm: LeanToTermMonix, mods: Vector[Modification]): Task[LeanToTermMonix]
  26. def withAxiomSeq(axs: Vector[(Name, Expr)], ltmT: Task[LeanToTermMonix], mods: Vector[Modification]): Task[LeanToTermMonix]
  27. def withDefn(name: Name, exp: Expr, ltm: LeanToTermMonix, mods: Vector[Modification]): Task[LeanToTermMonix]
  28. def withMod(mod: Modification, ltm: LeanToTermMonix, mods: Vector[Modification]): Task[LeanToTermMonix]