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. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from LeanParserEq toany2stringadd[LeanParserEq] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (LeanParserEq, B)
    Implicit
    This member is added by an implicit conversion from LeanParserEq toArrowAssoc[LeanParserEq] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. def addMods(m: Seq[Modification]): Unit
    Definition Classes
    LeanParser
  7. def allIndNames: ArrayBuffer[Name]
    Definition Classes
    LeanParser
  8. val allIntros: ArrayBuffer[(Name, Expr)]
    Definition Classes
    LeanParser
  9. def allNames(init: String = ""): ArrayBuffer[String]
    Definition Classes
    LeanParser
  10. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  12. def codeFromInd(ind: TermIndMod): Term
    Definition Classes
    LeanParser
  13. def codeGen: CodeGen
    Definition Classes
    LeanParser
  14. def defFromMod(name: Name): Option[Task[Term]]
    Definition Classes
    LeanParser
  15. def defFromModEq(name: Name): Option[Task[(Term, Set[EquationNode])]]
  16. def defNames: ArrayBuffer[Name]
    Definition Classes
    LeanParser
  17. def defnCode: ArrayBuffer[(Name, Term)]
    Definition Classes
    LeanParser
  18. val defnMap: Map[Name, Term]
    Definition Classes
    LeanParser
  19. val defnMapEq: Map[Name, (Term, Set[EquationNode])]
  20. def ensuring(cond: (LeanParserEq) => Boolean, msg: => Any): LeanParserEq
    Implicit
    This member is added by an implicit conversion from LeanParserEq toEnsuring[LeanParserEq] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  21. def ensuring(cond: (LeanParserEq) => Boolean): LeanParserEq
    Implicit
    This member is added by an implicit conversion from LeanParserEq toEnsuring[LeanParserEq] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  22. def ensuring(cond: Boolean, msg: => Any): LeanParserEq
    Implicit
    This member is added by an implicit conversion from LeanParserEq toEnsuring[LeanParserEq] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  23. def ensuring(cond: Boolean): LeanParserEq
    Implicit
    This member is added by an implicit conversion from LeanParserEq toEnsuring[LeanParserEq] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  24. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  25. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  26. def findChildren(name: Name): Option[Vector[Expr]]
    Definition Classes
    LeanParser
  27. def findDef(s: String): Option[DefMod]
    Definition Classes
    LeanParser
  28. def findDefMod(name: Name): Option[DefMod]
    Definition Classes
    LeanParser
  29. def findInd(s: String): Option[IndMod]
    Definition Classes
    LeanParser
  30. def findIndMod(name: Name): Option[IndMod]
    Definition Classes
    LeanParser
  31. def findIntro(name: Name): Option[Expr]
    Definition Classes
    LeanParser
  32. def findMod(name: Name, mods: Seq[Modification]): Option[Modification]
    Definition Classes
    LeanParser
  33. def findRecChildren(name: Name): Option[Vector[Expr]]
    Definition Classes
    LeanParser
  34. def foldAxiomSeq(accum: Vector[Term], axs: Vector[(Name, Expr)]): Task[Vector[Term]]
    Definition Classes
    LeanParser
  35. def foldAxiomSeqEq(accum: (Vector[Term], Set[EquationNode]), axs: Vector[(Name, Expr)]): Task[(Vector[Term], Set[EquationNode])]
  36. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from LeanParserEq toStringFormat[LeanParserEq] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  37. def funcFoldEqs(fn: Term, depth: Int, args: Vector[Term], result: Term): Set[EquationNode]
  38. def get(name: String): Term
    Definition Classes
    LeanParser
  39. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  40. def getEq(name: String): (Term, Set[EquationNode])
  41. def getEqError(name: String): Option[ParseException]
  42. def getEqFut(name: String): CancelableFuture[(Term, Set[EquationNode])]
  43. def getEqTask(name: String): Task[(Term, Set[EquationNode])]
  44. def getEqTry(name: String): Try[(Term, Set[EquationNode])]
  45. def getError(name: String): Option[ParseException]
    Definition Classes
    LeanParser
  46. def getFut(name: String): CancelableFuture[Term]
    Definition Classes
    LeanParser
  47. def getInd(s: String): TermIndMod
    Definition Classes
    LeanParser
  48. def getIndTask(s: String): Task[TermIndMod]
    Definition Classes
    LeanParser
  49. def getMemTermIndMod(name: Name, exp: Expr): Task[TermIndMod]
    Definition Classes
    LeanParser
  50. def getMemTermIndModEq(name: Name, exp: Expr): Task[TermIndMod]
  51. def getNamed(name: Name): Option[Task[Term]]
    Definition Classes
    LeanParser
  52. def getNamedEq(name: Name): Option[Task[(Term, Set[EquationNode])]]
  53. def getTask(name: String): Task[Term]
    Definition Classes
    LeanParser
  54. def getTermIndMod(name: Name): Option[Task[TermIndMod]]
    Definition Classes
    LeanParser
  55. def getTry(name: String): Try[Term]
    Definition Classes
    LeanParser
  56. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  57. def indModFromMod(name: Name): Option[Task[TermIndMod]]
    Definition Classes
    LeanParser
  58. def indModFromModEq(name: Name): Option[Task[TermIndMod]]
  59. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  60. def maxIndex(exp: Expr): Int
    Definition Classes
    LeanParser
  61. def modNames(mod: Modification): Vector[Name]
    Definition Classes
    LeanParser
  62. val mods: ArrayBuffer[Modification]
    Definition Classes
    LeanParser
  63. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  64. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  65. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  66. def parse(exp: Expr, vars: Vector[Term] = Vector()): Task[Term]
    Definition Classes
    LeanParser
  67. def parseEq(exp: Expr, vars: Vector[Term] = Vector()): Task[(Term, Set[EquationNode])]
  68. val parseMemo: Map[(Expr, Vector[Term]), Term]
    Definition Classes
    LeanParser
  69. def parseOptVec(vec: Vector[(Expr, Int)], vars: Vector[Term], indices: Set[Int]): Task[Vector[Option[Term]]]
    Definition Classes
    LeanParser
  70. def parseVec(vec: Vector[Expr], vars: Vector[Term]): Task[Vector[Term]]
    Definition Classes
    LeanParser
  71. def parseVecEq(vec: Vector[Expr], vars: Vector[Term]): Task[(Vector[Term], Set[EquationNode])]
  72. def recApp(name: Name, args: Vector[Expr], exp: Expr, vars: Vector[Term]): Task[Term]
    Definition Classes
    LeanParser
  73. def recAppEq(name: Name, args: Vector[Expr], exp: Expr, vars: Vector[Term]): Task[(Term, Set[EquationNode])]
  74. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  75. val termIndModMap: Map[Name, TermIndMod]
    Definition Classes
    LeanParser
  76. def toString(): String
    Definition Classes
    AnyRef → Any
  77. def topNames(init: String = ""): ArrayBuffer[String]
    Definition Classes
    LeanParser
  78. def update(): Unit
    Definition Classes
    LeanParser
  79. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  80. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  81. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  82. def withAxiom(name: Name, ty: Expr): Task[Unit]
    Definition Classes
    LeanParser
  83. def withAxiomEq(name: Name, ty: Expr): Task[Unit]
  84. def withAxiomSeq(axs: Vector[(Name, Expr)]): Task[Unit]
    Definition Classes
    LeanParser
  85. def withAxiomSeqEq(axs: Vector[(Name, Expr)]): Task[Unit]
  86. def withDefn(name: Name, exp: Expr): Task[Unit]
    Definition Classes
    LeanParser
  87. def withDefnEq(name: Name, exp: Expr): Task[Unit]
  88. def withMod(mod: Modification): Task[Unit]
    Definition Classes
    LeanParser
  89. def withModEq(mod: Modification): Task[Unit]

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated
  2. def →[B](y: B): (LeanParserEq, B)
    Implicit
    This member is added by an implicit conversion from LeanParserEq toArrowAssoc[LeanParserEq] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @deprecated
    Deprecated

    (Since version 2.13.0) Use -> instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.

Inherited from LeanParser

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd fromLeanParserEq to any2stringadd[LeanParserEq]

Inherited by implicit conversion StringFormat fromLeanParserEq to StringFormat[LeanParserEq]

Inherited by implicit conversion Ensuring fromLeanParserEq to Ensuring[LeanParserEq]

Inherited by implicit conversion ArrowAssoc fromLeanParserEq to ArrowAssoc[LeanParserEq]

Ungrouped