Packages

trait LeanParse extends AnyRef

Self Type
LeanParse
Linear Supertypes
AnyRef, Any
Known Subclasses
LeanToTerm, LeanToTermMut
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanParse
  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

Abstract Value Members

  1. abstract def addAxiom(name: Name, exp: Expr): LeanParse
  2. abstract def addAxiomOpt(name: Name, exp: Expr): LeanParse
  3. abstract def addDefnVal(name: Name, ty: Expr, value: Expr): LeanParse
  4. abstract def addDefnValOpt(name: Name, ty: Expr, value: Expr): LeanParse
  5. abstract val defnMap: Map[Name, Term]
  6. abstract val termIndModMap: Map[Name, TermIndMod]

Concrete Value Members

  1. def applyFuncProp(func: Term, arg: Term, vars: Vector[Term], data: Vector[Expr] = Vector()): Term
  2. def applyFuncPropOpt(func: Term, arg: Term): Option[Term]
  3. def defnOpt(exp: Expr): Option[Term]
  4. def defns(exp: Expr, typOpt: Option[Typ[Term]]): Option[Term]
  5. val inPropFamily: (Term) => Boolean
  6. val parse: Parser
  7. val parseOpt: OptParser
  8. def parseSym(name: Name, ty: Expr, vars: Vector[Term]): Try[Term]
  9. def parseSymOpt(name: Name, ty: Expr, vars: Vector[Term]): Option[U forSome {type U <: Term with Subs[U]}]
  10. def parseSymVec(vec: Vector[(Name, Expr)], vars: Vector[Term]): Try[Vector[Term]]
  11. def parseSymVecOpt(vec: Vector[(Name, Expr)], vars: Vector[Term]): Option[Vector[Term]]
  12. def parseTyp(x: Expr, vars: Vector[Term]): Try[Typ[Term]]
  13. def parseTypOpt(x: Expr, vars: Vector[Term]): Option[Typ[U] forSome {type U <: Term with Subs[U]}]
  14. def parseTypVec(vec: Vector[Expr], vars: Vector[Term]): Try[Vector[Typ[Term]]]
  15. def parseVar(b: Binding, vars: Vector[Term]): Try[Term]
  16. def parseVec(vec: Vector[Expr], vars: Vector[Term]): Try[Vector[Term]]
  17. def parseVecOpt(vec: Vector[Expr], vars: Vector[Term]): Option[Vector[Term]]
  18. def recOptParser(rec: => OptParser)(exp: Expr, vars: Vector[Term]): Option[Term]
  19. def recParser(rec: => Parser)(exp: Expr, vars: Vector[Term]): Try[Term]
  20. def toTermIndModOpt(ind: IndMod): Option[TermIndMod]
  21. def toTermIndModTry(ind: IndMod): Try[TermIndMod]
  22. object Predef