Packages

object ScalaUniv extends Serializable

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

Type Members

  1. case class FineSymbTyp[U <: Term with Subs[U]](name: AnySym, symobj: (AnySym) => U) extends Typ[U] with Symbolic with Product with Serializable

    Symbolic types, which the compiler knows are types.

  2. case class FineUniv[U <: Term with Subs[U]](symobj: (AnySym) => U) extends Typ[Typ[U]] with BaseUniv with Product with Serializable
  3. case class FuncTypUniv[W <: Term with Subs[W], U <: Term with Subs[U]](domuniv: Typ[Typ[W]], codomuniv: Typ[Typ[U]]) extends Typ[FuncTyp[W, U]] with Product with Serializable

    Universe whose elements are FuncTyps

  4. case class HigherUniv[U <: Typ[Term] with Subs[U]](univ: Typ[U]) extends Typ[Typ[U]] with Product with Serializable

    given a universe with objects of scala type Typ[U], gives one with scala type Typ[Typ[U]]

Deprecated Type Members

  1. case class PiTypUniv[W <: Term with Subs[W], U <: Term with Subs[U]](domuniv: Typ[Typ[W]], codomuniv: Typ[Typ[U]]) extends Typ[PiTyp[W, U]] with Product with Serializable

    Universe with objects Pi-Types

    Universe with objects Pi-Types

    Annotations
    @deprecated
    Deprecated

    (Since version 14/12/2016) Use PiDefn

Value Members

  1. implicit val baseUniv: ScalaUniv[Term]

    scala universe with no refinement.

  2. def depFunc[W <: Term with Subs[W], U <: Term with Subs[U]](dom: Typ[W], func: (W) => U)(implicit su: ScalaUniv[U]): FuncLike[W, U]

    returns dependent function inferring type fiber.

  3. implicit def funcUniv[W <: Term with Subs[W], U <: Term with Subs[U]](implicit domsc: ScalaUniv[W], codomsc: ScalaUniv[U]): ScalaUniv[Func[W, U]]

    implicitly build universe with elements FuncTyps from universes for domain and codomain.

  4. implicit def higherUniv[U <: Term with Subs[U]](implicit sc: ScalaUniv[U]): ScalaUniv[Typ[U]]

    implicitly returns from a scala universe of Typ[U] one of Typ[Typ[U]]

  5. def newobj: Nothing
  6. def typFamily[W <: Term with Subs[W], U <: Term with Subs[U]](dom: Typ[W], f: (W) => Typ[U])(implicit su: ScalaUniv[U]): FuncDefn[W, Typ[U]]

    create type family, implicitly using a scala-universe object to build the codomain.

  7. object DepFunc

    Companion to dependent functions

Deprecated Value Members

  1. implicit def piUniv[W <: Term with Subs[W], U <: Term with Subs[U]](implicit domsc: ScalaUniv[W], codomsc: ScalaUniv[U]): ScalaUniv[FuncLike[W, U]]

    builds scala universe for pi-types given ones for domain and codomain types.

    builds scala universe for pi-types given ones for domain and codomain types.

    Annotations
    @deprecated
    Deprecated

    (Since version 14/12/2016) Use PiDefn