object LeanInterface
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- LeanInterface
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def applyFuncLean(func: Term, arg: Term): Term
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- def consts(expr: Expr): Vector[Name]
- def defnExprs(mods: Vector[Modification]): Vector[Expr]
- def defnNames(mods: Vector[Modification], accum: Vector[Name] = Vector()): Vector[Name]
- Annotations
- @tailrec()
- def domVarFlag(introTyp: Typ[Term], typF: Term): Vector[Boolean]
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def foldFuncLean(func: Term, args: Vector[Term]): Term
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def getMods(filename: String): Vector[Modification]
- def getModsFromStream(in: InputStream): Vector[Modification]
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- 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
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def modSubExpr: (Modification) => Set[Expr]
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def recApp: (Expr) => Boolean
- def subExpr(expr: Expr): Vector[Expr]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- def unifier(a: Term, b: Term, numParams: Int, accum: Vector[(Term, Term)] = Vector()): Option[Vector[(Term, Term)]]
- def usesVar(expr: Expr, index: Int, ignoreTypes: Boolean = false): Boolean
- def varsUsed(expr: Expr): Set[Int]
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- def witLess(t: Term): Vector[Term]
fill in witnesses if proposition, including within lambdas
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated