Packages

case class LeanToTermMut(defnMap: Map[Name, Term], termIndModMap: Map[Name, TermIndMod], unparsed: ArrayBuffer[Name] = ArrayBuffer()) extends LeanParse with Product with Serializable

Self Type
LeanToTermMut
Linear Supertypes
Serializable, Product, Equals, LeanParse, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanToTermMut
  2. Serializable
  3. Product
  4. Equals
  5. LeanParse
  6. AnyRef
  7. 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 LeanToTermMut(defnMap: Map[Name, Term], termIndModMap: Map[Name, TermIndMod], unparsed: ArrayBuffer[Name] = ArrayBuffer())

Value Members

  1. object Predef
    Definition Classes
    LeanParse
  2. def add(mod: Modification): LeanParse
  3. def addAxiom(name: Name, ty: Expr): LeanParse
    Definition Classes
    LeanToTermMut → LeanParse
  4. def addAxiomMod(ax: AxiomMod): LeanParse
  5. def addAxiomModOpt(ax: AxiomMod): LeanParse
  6. def addAxiomOpt(name: Name, ty: Expr): LeanParse
    Definition Classes
    LeanToTermMut → LeanParse
  7. def addAxioms(axs: Vector[(Name, Expr)]): LeanParse
  8. def addAxiomsOpt(axs: Vector[(Name, Expr)]): LeanToTermMut
  9. def addDefMod(df: DefMod): LeanParse
  10. def addDefModOpt(df: DefMod): LeanParse
  11. def addDefnMap(name: Name, term: Term): LeanParse
  12. def addDefnVal(name: Name, value: Expr, tp: Expr): LeanParse
    Definition Classes
    LeanToTermMut → LeanParse
  13. def addDefnValOpt(name: Name, value: Expr, tp: Expr): LeanParse
    Definition Classes
    LeanToTermMut → LeanParse
  14. def addIndMod(ind: IndMod): LeanParse
  15. def addIndModOpt(ind: IndMod): LeanParse
  16. def addOpt(mod: Modification): LeanParse
  17. def addQuotMod: LeanParse
  18. def addQuotModOpt: LeanParse
  19. def applyFuncProp(func: Term, arg: Term, vars: Vector[Term], data: Vector[Expr] = Vector()): Term
    Definition Classes
    LeanParse
  20. def applyFuncPropOpt(func: Term, arg: Term): Option[Term]
    Definition Classes
    LeanParse
  21. val defnMap: Map[Name, Term]
    Definition Classes
    LeanToTermMut → LeanParse
  22. def defnOpt(exp: Expr): Option[Term]
    Definition Classes
    LeanParse
  23. def defns(exp: Expr, typOpt: Option[Typ[Term]]): Option[Term]
    Definition Classes
    LeanParse
  24. val inPropFamily: (Term) => Boolean
    Definition Classes
    LeanParse
  25. val parse: Parser
    Definition Classes
    LeanParse
  26. val parseOpt: OptParser
    Definition Classes
    LeanParse
  27. def parseSym(name: Name, ty: Expr, vars: Vector[Term]): Try[Term]
    Definition Classes
    LeanParse
  28. def parseSymOpt(name: Name, ty: Expr, vars: Vector[Term]): Option[U forSome {type U <: Term with Subs[U]}]
    Definition Classes
    LeanParse
  29. def parseSymVec(vec: Vector[(Name, Expr)], vars: Vector[Term]): Try[Vector[Term]]
    Definition Classes
    LeanParse
  30. def parseSymVecOpt(vec: Vector[(Name, Expr)], vars: Vector[Term]): Option[Vector[Term]]
    Definition Classes
    LeanParse
  31. def parseTyp(x: Expr, vars: Vector[Term]): Try[Typ[Term]]
    Definition Classes
    LeanParse
  32. def parseTypOpt(x: Expr, vars: Vector[Term]): Option[Typ[U] forSome {type U <: Term with Subs[U]}]
    Definition Classes
    LeanParse
  33. def parseTypVec(vec: Vector[Expr], vars: Vector[Term]): Try[Vector[Typ[Term]]]
    Definition Classes
    LeanParse
  34. def parseVar(b: Binding, vars: Vector[Term]): Try[Term]
    Definition Classes
    LeanParse
  35. def parseVec(vec: Vector[Expr], vars: Vector[Term]): Try[Vector[Term]]
    Definition Classes
    LeanParse
  36. def parseVecOpt(vec: Vector[Expr], vars: Vector[Term]): Option[Vector[Term]]
    Definition Classes
    LeanParse
  37. def productElementNames: Iterator[String]
    Definition Classes
    Product
  38. def putAxiom(name: Name, ty: Expr): Unit
  39. def putAxiomOpt(name: Name, ty: Expr): Unit
  40. def recOptParser(rec: => OptParser)(exp: Expr, vars: Vector[Term]): Option[Term]
    Definition Classes
    LeanParse
  41. def recParser(rec: => Parser)(exp: Expr, vars: Vector[Term]): Try[Term]
    Definition Classes
    LeanParse
  42. val termIndModMap: Map[Name, TermIndMod]
    Definition Classes
    LeanToTermMut → LeanParse
  43. def toTermIndModOpt(ind: IndMod): Option[TermIndMod]
    Definition Classes
    LeanParse
  44. def toTermIndModTry(ind: IndMod): Try[TermIndMod]
    Definition Classes
    LeanParse
  45. val unparsed: ArrayBuffer[Name]