Packages

object LeanInterface

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

Value Members

  1. def applyFuncLean(func: Term, arg: Term): Term
  2. def consts(expr: Expr): Vector[Name]
  3. def defnExprs(mods: Vector[Modification]): Vector[Expr]
  4. def defnNames(mods: Vector[Modification], accum: Vector[Name] = Vector()): Vector[Name]
    Annotations
    @tailrec()
  5. def domVarFlag(introTyp: Typ[Term], typF: Term): Vector[Boolean]
  6. def foldFuncLean(func: Term, args: Vector[Term]): Term
  7. def getMods(filename: String): Vector[Modification]
  8. def getModsFromStream(in: InputStream): Vector[Modification]
  9. def introShuffle(intro: Term, typF: Term, data: Term, numParams: Int): Term

    shuffles the dat variables from leans convention where they are last to an interleaved form.

    shuffles the dat variables from leans convention where they are last to an interleaved form.

    intro

    the introduction rule

    typF

    the inductive type

    data

    the recursion data

  10. def modSubExpr: (Modification) => Set[Expr]
  11. def recApp: (Expr) => Boolean
  12. def subExpr(expr: Expr): Vector[Expr]
  13. def unifier(a: Term, b: Term, numParams: Int, accum: Vector[(Term, Term)] = Vector()): Option[Vector[(Term, Term)]]
  14. def usesVar(expr: Expr, index: Int, ignoreTypes: Boolean = false): Boolean
  15. def varsUsed(expr: Expr): Set[Int]
  16. def witLess(t: Term): Vector[Term]

    fill in witnesses if proposition, including within lambdas