Packages

object LeanToTerm extends Serializable

Linear Supertypes
Serializable, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LeanToTerm
  2. Serializable
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type OptParser = (Expr, Vector[Term]) => Option[Term]
  2. type Parser = (Expr, Vector[Term]) => Try[Term]
  3. type TypedParser = (Expr, Option[Typ[Term]]) => Option[Term]

Value Members

  1. val appFailure: ArrayBuffer[(Expr, Expr, Expr, Option[Typ[Term]], LeanToTerm)]
  2. val badConsts: ArrayBuffer[Const]
  3. val empty: LeanToTerm
  4. def emptyRecParser(base: => Parser)(e: Expr, vars: Vector[Term]): None
  5. def fromMods(mods: Vector[Modification], init: LeanToTerm = empty): LeanToTerm
  6. def fromModsOpt(mods: Vector[Modification], init: LeanToTerm = empty): LeanToTerm
  7. def getValue(t: Term, n: Int, accum: Vector[Term]): Try[(Term, Vector[Term])]
  8. def getValueOpt(t: Term, n: Int, accum: Vector[Term]): Option[(Term, Vector[Term])]
  9. val isPropn: (Expr) => Boolean
  10. def iterAp(name: Name, length: Int): (Expr) => Option[Vector[Expr]]
  11. def iterApTyp(name: Name, length: Int, typOpt: Option[Typ[Term]]): (Expr) => Option[Vector[(Expr, Option[Typ[Term]])]]
  12. def iterMods(mods: Vector[Modification], init: LeanToTerm = empty): Iterator[LeanToTerm]
  13. def iterModsOpt(mods: Vector[Modification], init: LeanToTerm = empty): Iterator[LeanToTerm]
  14. def optSequence[A](vec: Vector[Option[A]]): Option[Vector[A]]
  15. object RecIterAp