trait ExprLang[E] extends AnyRef
Abstraction (as a type class) of a language for mathematical expressions, i.e., of
* methods for forming expressions, * some basic expressions such as true, false, numbers etc.
Expression include functions and propositions. However, expressions here need not include sophisticated, and foundation specific, constructions such as inductive types; these should be abstracted separately.
While the design is based on homotopy type theory, implementations can be with a range of logics or functional languages, for instance HOL or the Wolfram language. All methods are optional, so anything outside a language is just not built.
This is integrated with and used by many components.
* As a target for natural language and latex translation. * Bidirectional integration with HoTT implementations: * * terms have such a structure, * * terms can be translated to a language with this structure. * Allows pickling of terms by implementing a formal expression language. * _Goal:_ Bidirectional integration with lean expressions.
- Alphabetic
- By Inheritance
- ExprLang
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Abstract Value Members
- abstract def anonVar(typ: E): Option[E]
anonymous variable
- abstract def appln(func: E, arg: E): Option[E]
- abstract def equality(lhs: E, rhs: E): Option[E]
- abstract def ff: Option[E]
false type
- abstract def incl1(typ: E): Option[E]
- abstract def incl2(typ: E): Option[E]
- abstract def lambda(variable: E, value: E): Option[E]
- abstract def metaVar(typ: E): Option[E]
meta-variable of a given type, i.e., whose value must be inferred (elaborated in lean's terminology).
- abstract def numeral(n: Int): Option[E]
- abstract def or(first: E, second: E): Option[E]
- abstract def orCases(first: E, second: E): Option[E]
- abstract def pair(x: E, y: E): Option[E]
- abstract def pi(variable: E, typ: E): Option[E]
- abstract def proj1(xy: E): Option[E]
- abstract def proj2(xy: E): Option[E]
- abstract def qed: Option[E]
element of true type
- abstract def sigma(variable: E, typFamily: E): Option[E]
- abstract def tt: Option[E]
true type
- abstract def typVariable[S](name: S, level: Int): Option[E]
- abstract def variable[S](name: S, typ: E): Option[E]
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (ExprLang[E], B)
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def applyAll(funcOpt: Option[E], args: Vector[E]): Option[E]
- 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 ensuring(cond: (ExprLang[E]) => Boolean, msg: => Any): ExprLang[E]
- def ensuring(cond: (ExprLang[E]) => Boolean): ExprLang[E]
- def ensuring(cond: Boolean, msg: => Any): ExprLang[E]
- def ensuring(cond: Boolean): ExprLang[E]
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def formatted(fmtstr: String): String
- def funcTyp(dom: E, codom: E): Option[E]
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def i1(typ: E, value: E): Option[E]
- def i2(typ: E, value: E): Option[E]
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- 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 pairTyp(first: E, second: E): Option[E]
non-dependent pair built from abstract methods.
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- 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])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def →[B](y: B): (ExprLang[E], B)
- Implicit
- This member is added by an implicit conversion from ExprLang[E] toArrowAssoc[ExprLang[E]] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.