Packages

class LeanParserEq extends LeanParser

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

Value Members

  1. def addMods(m: Seq[Modification]): Unit
    Definition Classes
    LeanParser
  2. def allIndNames: ArrayBuffer[Name]
    Definition Classes
    LeanParser
  3. val allIntros: ArrayBuffer[(Name, Expr)]
    Definition Classes
    LeanParser
  4. def allNames(init: String = ""): ArrayBuffer[String]
    Definition Classes
    LeanParser
  5. def codeFromInd(ind: TermIndMod): Term
    Definition Classes
    LeanParser
  6. def codeGen: CodeGen
    Definition Classes
    LeanParser
  7. def defFromMod(name: Name): Option[Task[Term]]
    Definition Classes
    LeanParser
  8. def defFromModEq(name: Name): Option[Task[(Term, Set[EquationNode])]]
  9. def defNames: ArrayBuffer[Name]
    Definition Classes
    LeanParser
  10. def defnCode: ArrayBuffer[(Name, Term)]
    Definition Classes
    LeanParser
  11. val defnMap: Map[Name, Term]
    Definition Classes
    LeanParser
  12. val defnMapEq: Map[Name, (Term, Set[EquationNode])]
  13. def findChildren(name: Name): Option[Vector[Expr]]
    Definition Classes
    LeanParser
  14. def findDef(s: String): Option[DefMod]
    Definition Classes
    LeanParser
  15. def findDefMod(name: Name): Option[DefMod]
    Definition Classes
    LeanParser
  16. def findInd(s: String): Option[IndMod]
    Definition Classes
    LeanParser
  17. def findIndMod(name: Name): Option[IndMod]
    Definition Classes
    LeanParser
  18. def findIntro(name: Name): Option[Expr]
    Definition Classes
    LeanParser
  19. def findMod(name: Name, mods: Seq[Modification]): Option[Modification]
    Definition Classes
    LeanParser
  20. def findRecChildren(name: Name): Option[Vector[Expr]]
    Definition Classes
    LeanParser
  21. def foldAxiomSeq(accum: Vector[Term], axs: Vector[(Name, Expr)]): Task[Vector[Term]]
    Definition Classes
    LeanParser
  22. def foldAxiomSeqEq(accum: (Vector[Term], Set[EquationNode]), axs: Vector[(Name, Expr)]): Task[(Vector[Term], Set[EquationNode])]
  23. def funcFoldEqs(fn: Term, depth: Int, args: Vector[Term], result: Term): Set[EquationNode]
  24. def get(name: String): Term
    Definition Classes
    LeanParser
  25. def getEq(name: String): (Term, Set[EquationNode])
  26. def getEqError(name: String): Option[ParseException]
  27. def getEqFut(name: String): CancelableFuture[(Term, Set[EquationNode])]
  28. def getEqTask(name: String): Task[(Term, Set[EquationNode])]
  29. def getEqTry(name: String): Try[(Term, Set[EquationNode])]
  30. def getError(name: String): Option[ParseException]
    Definition Classes
    LeanParser
  31. def getFut(name: String): CancelableFuture[Term]
    Definition Classes
    LeanParser
  32. def getInd(s: String): TermIndMod
    Definition Classes
    LeanParser
  33. def getIndTask(s: String): Task[TermIndMod]
    Definition Classes
    LeanParser
  34. def getMemTermIndMod(name: Name, exp: Expr): Task[TermIndMod]
    Definition Classes
    LeanParser
  35. def getMemTermIndModEq(name: Name, exp: Expr): Task[TermIndMod]
  36. def getNamed(name: Name): Option[Task[Term]]
    Definition Classes
    LeanParser
  37. def getNamedEq(name: Name): Option[Task[(Term, Set[EquationNode])]]
  38. def getTask(name: String): Task[Term]
    Definition Classes
    LeanParser
  39. def getTermIndMod(name: Name): Option[Task[TermIndMod]]
    Definition Classes
    LeanParser
  40. def getTry(name: String): Try[Term]
    Definition Classes
    LeanParser
  41. def indModFromMod(name: Name): Option[Task[TermIndMod]]
    Definition Classes
    LeanParser
  42. def indModFromModEq(name: Name): Option[Task[TermIndMod]]
  43. def maxIndex(exp: Expr): Int
    Definition Classes
    LeanParser
  44. def modNames(mod: Modification): Vector[Name]
    Definition Classes
    LeanParser
  45. val mods: ArrayBuffer[Modification]
    Definition Classes
    LeanParser
  46. def parse(exp: Expr, vars: Vector[Term] = Vector()): Task[Term]
    Definition Classes
    LeanParser
  47. def parseEq(exp: Expr, vars: Vector[Term] = Vector()): Task[(Term, Set[EquationNode])]
  48. val parseMemo: Map[(Expr, Vector[Term]), Term]
    Definition Classes
    LeanParser
  49. def parseOptVec(vec: Vector[(Expr, Int)], vars: Vector[Term], indices: Set[Int]): Task[Vector[Option[Term]]]
    Definition Classes
    LeanParser
  50. def parseVec(vec: Vector[Expr], vars: Vector[Term]): Task[Vector[Term]]
    Definition Classes
    LeanParser
  51. def parseVecEq(vec: Vector[Expr], vars: Vector[Term]): Task[(Vector[Term], Set[EquationNode])]
  52. def recApp(name: Name, args: Vector[Expr], exp: Expr, vars: Vector[Term]): Task[Term]
    Definition Classes
    LeanParser
  53. def recAppEq(name: Name, args: Vector[Expr], exp: Expr, vars: Vector[Term]): Task[(Term, Set[EquationNode])]
  54. val termIndModMap: Map[Name, TermIndMod]
    Definition Classes
    LeanParser
  55. def topNames(init: String = ""): ArrayBuffer[String]
    Definition Classes
    LeanParser
  56. def update(): Unit
    Definition Classes
    LeanParser
  57. def withAxiom(name: Name, ty: Expr): Task[Unit]
    Definition Classes
    LeanParser
  58. def withAxiomEq(name: Name, ty: Expr): Task[Unit]
  59. def withAxiomSeq(axs: Vector[(Name, Expr)]): Task[Unit]
    Definition Classes
    LeanParser
  60. def withAxiomSeqEq(axs: Vector[(Name, Expr)]): Task[Unit]
  61. def withDefn(name: Name, exp: Expr): Task[Unit]
    Definition Classes
    LeanParser
  62. def withDefnEq(name: Name, exp: Expr): Task[Unit]
  63. def withMod(mod: Modification): Task[Unit]
    Definition Classes
    LeanParser
  64. def withModEq(mod: Modification): Task[Unit]