Packages

trait ScalaRep[+U <: Term with Subs[U], V] extends AnyRef

Representation by a scala object of a HoTT term

It is assumed that there is a single HoTT type corresponding to the given scala type, when the scala rep is in scope. If one needs several HoTT types, eg. vectors of different lengths, one uses ScalaPolyRep.

ScalaRep objects are recursively constructed from

U

the HoTT type represented

V

scala type representing the given object.

Linear Supertypes
AnyRef, Any
Known Subclasses
EnumRep, ListRep, DepFuncRep, FuncRep, IdRep, IdTypRep, SigmaRep, SimpleRep, SmpleFuncRep
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ScalaRep
  2. AnyRef
  3. Any
Implicitly
  1. by ScalaTerm
  2. by any2stringadd
  3. by StringFormat
  4. by Ensuring
  5. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type tpe = V

    scala type of representing object.

Abstract Value Members

  1. abstract def apply(v: V): U

    HoTT object from the scala one.

  2. abstract def subs(x: Term, y: Term): ScalaRep[U, V]
  3. abstract val typ: Typ[U]

    HoTT type represented.

  4. abstract def unapply(u: Term): Option[V]

    pattern for matching application of the scala object.

Concrete Value Members

  1. def ++[UU >: U <: Term with Subs[UU], X <: Term with Subs[X], Y](codrepfmly: (V) => ScalaRep[X, Y]): SigmaRep[UU, V, X, Y]

    scalarep for sum type.

  2. def -->:[W <: Term with Subs[W], X, UU >: U <: Term with Subs[UU]](that: ScalaRep[W, X]): FuncRep[W, X, UU, V]

    scalarep for function

  3. def :-->[W <: Term with Subs[W], UU >: U <: Term with Subs[UU]](that: Typ[W]): FuncRep[UU, V, W, W]
  4. def term: U
    Implicit
    This member is added by an implicit conversion from ScalaRep[U, V] toScalaTerm[U, ScalaRep[U, V]] performed by method ScalaTerm in provingground.scalahott.ScalaRep.This conversion will take place only if an implicit value of type ScalaRep[U, ScalaRep[U, V]] is in scope.
    Definition Classes
    ScalaTerm