Packages

class LeanParser extends AnyRef

Linear Supertypes
AnyRef, Any
Known Subclasses
LeanParserEq
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanParser
  2. AnyRef
  3. 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 LeanParser(initMods: Seq[Modification], defTaskMap: Map[Name, Task[Term]] = Map(), indTaskMap: Map[Name, Task[TermIndMod]] = Map(), log: Logger = LeanParser.Logger.nop)

Value Members

  1. def addMods(m: Seq[Modification]): Unit
  2. def allIndNames: ArrayBuffer[Name]
  3. val allIntros: ArrayBuffer[(Name, Expr)]
  4. def allNames(init: String = ""): ArrayBuffer[String]
  5. def codeFromInd(ind: TermIndMod): Term
  6. def codeGen: CodeGen
  7. def defFromMod(name: Name): Option[Task[Term]]
  8. def defNames: ArrayBuffer[Name]
  9. def defnCode: ArrayBuffer[(Name, Term)]
  10. val defnMap: Map[Name, Term]
  11. def findChildren(name: Name): Option[Vector[Expr]]
  12. def findDef(s: String): Option[DefMod]
  13. def findDefMod(name: Name): Option[DefMod]
  14. def findInd(s: String): Option[IndMod]
  15. def findIndMod(name: Name): Option[IndMod]
  16. def findIntro(name: Name): Option[Expr]
  17. def findMod(name: Name, mods: Seq[Modification]): Option[Modification]
  18. def findRecChildren(name: Name): Option[Vector[Expr]]
  19. def foldAxiomSeq(accum: Vector[Term], axs: Vector[(Name, Expr)]): Task[Vector[Term]]
  20. def get(name: String): Term
  21. def getError(name: String): Option[ParseException]
  22. def getFut(name: String): CancelableFuture[Term]
  23. def getInd(s: String): TermIndMod
  24. def getIndTask(s: String): Task[TermIndMod]
  25. def getMemTermIndMod(name: Name, exp: Expr): Task[TermIndMod]
  26. def getNamed(name: Name): Option[Task[Term]]
  27. def getTask(name: String): Task[Term]
  28. def getTermIndMod(name: Name): Option[Task[TermIndMod]]
  29. def getTry(name: String): Try[Term]
  30. def indModFromMod(name: Name): Option[Task[TermIndMod]]
  31. def maxIndex(exp: Expr): Int
  32. def modNames(mod: Modification): Vector[Name]
  33. val mods: ArrayBuffer[Modification]
  34. def parse(exp: Expr, vars: Vector[Term] = Vector()): Task[Term]
  35. val parseMemo: Map[(Expr, Vector[Term]), Term]
  36. def parseOptVec(vec: Vector[(Expr, Int)], vars: Vector[Term], indices: Set[Int]): Task[Vector[Option[Term]]]
  37. def parseVec(vec: Vector[Expr], vars: Vector[Term]): Task[Vector[Term]]
  38. def recApp(name: Name, args: Vector[Expr], exp: Expr, vars: Vector[Term]): Task[Term]
  39. val termIndModMap: Map[Name, TermIndMod]
  40. def topNames(init: String = ""): ArrayBuffer[String]
  41. def update(): Unit
  42. def withAxiom(name: Name, ty: Expr): Task[Unit]
  43. def withAxiomSeq(axs: Vector[(Name, Expr)]): Task[Unit]
  44. def withDefn(name: Name, exp: Expr): Task[Unit]
  45. def withMod(mod: Modification): Task[Unit]