Packages

object LeanParser

Linear Supertypes
AnyRef, Any
Content Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanParser
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. class ApplnParseException extends ApplnFailException
  2. case class Defined(name: Name, term: Term) extends Log with Product with Serializable
  3. case class DefinedInduc(name: Name, indMod: TermIndMod) extends Log with Product with Serializable
  4. case class LambdaFormException(variable: Term, value: Term, error: Throwable) extends Exception with Product with Serializable
  5. sealed trait Log extends AnyRef
  6. trait Logger extends (Log) => Unit
  7. case class ParseException(expVars: Vector[(Expr, Vector[Term])], error: Exception) extends Exception with Product with Serializable
  8. case class ParseWork(expr: Expr) extends Log with Product with Serializable
  9. case class Parsed(expr: Expr) extends Log with Product with Serializable

Value Members

  1. def apply(filename: String): LeanParser
  2. def applyFuncFold(ft: Task[Term], v: Vector[Term]): Task[Term]
  3. def applyFuncOptFold(ft: Task[Option[Term]], v: Vector[Option[Term]]): Task[Option[Term]]
  4. def getExstInduc(ind: TermIndMod, argsFmlyTerm: Vector[Term]): Task[ExstInducDefn]
  5. def getIndexedExstInduc(ind: IndexedIndMod, argsFmlyTerm: Task[Vector[Term]]): Task[ExstInducDefn]
  6. def getNextVarName(vecs: Vector[Term], n: Int): String
  7. def getRec(ind: TermIndMod, argsFmlyTerm: Vector[Term]): Task[Term]
  8. def getRecIndexed(ind: IndexedIndMod, argsFmlyTerm: Task[Vector[Term]]): Task[Term]
  9. def getRecSimple(ind: SimpleIndMod, argsFmlyTerm: Task[Vector[Term]]): Task[Term]
  10. def getSimpleExstInduc(ind: SimpleIndMod, argsFmlyTerm: Task[Vector[Term]]): Task[ExstInducDefn]
  11. def getValue(t: Term, n: Int, accum: Vector[Term]): Task[(Term, Vector[Term])]
  12. def introsFold(ind: TermIndMod, p: Vector[Term]): Vector[Term]
  13. def isPropnFn(e: Expr): Boolean
  14. def jsDef(parser: LeanParser): Arr
  15. def jsTermIndMod(parser: LeanParser): Arr
  16. def load(s: String = "basic"): LeanParser
  17. val parseWork: Set[Expr]
  18. def proofLift: (Term, Term) => Task[Term]
  19. def shiftedName(n: Int, lastName: String = "'"): String
    Annotations
    @tailrec()
  20. def splitVec[A](sizes: Vector[Int], vec: Vector[A]): (Vector[Vector[A]], Vector[A])
  21. def toJs(parser: LeanParser): Obj
  22. object Logger
  23. object RecIterAp