Packages

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.

Linear Supertypes
AnyRef, Any
Known Subclasses
StochasticLang, TruncatedDistributionLang, FreeLang, TermLang
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ExprLang
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Abstract Value Members

  1. abstract def anonVar(typ: E): Option[E]

    anonymous variable

  2. abstract def appln(func: E, arg: E): Option[E]
  3. abstract def equality(lhs: E, rhs: E): Option[E]
  4. abstract def ff: Option[E]

    false type

  5. abstract def incl1(typ: E): Option[E]
  6. abstract def incl2(typ: E): Option[E]
  7. abstract def lambda(variable: E, value: E): Option[E]
  8. 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).

  9. abstract def numeral(n: Int): Option[E]
  10. abstract def or(first: E, second: E): Option[E]
  11. abstract def orCases(first: E, second: E): Option[E]
  12. abstract def pair(x: E, y: E): Option[E]
  13. abstract def pi(variable: E, typ: E): Option[E]
  14. abstract def proj1(xy: E): Option[E]
  15. abstract def proj2(xy: E): Option[E]
  16. abstract def qed: Option[E]

    element of true type

  17. abstract def sigma(variable: E, typFamily: E): Option[E]
  18. abstract def tt: Option[E]

    true type

  19. abstract def typVariable[S](name: S, level: Int): Option[E]
  20. abstract def variable[S](name: S, typ: E): Option[E]

Concrete Value Members

  1. def applyAll(funcOpt: Option[E], args: Vector[E]): Option[E]
  2. def funcTyp(dom: E, codom: E): Option[E]
  3. def i1(typ: E, value: E): Option[E]
  4. def i2(typ: E, value: E): Option[E]
  5. def pairTyp(first: E, second: E): Option[E]

    non-dependent pair built from abstract methods.