Packages

case class PlusTyp[U <: Term with Subs[U], V <: Term with Subs[V]](first: Typ[U], second: Typ[V]) extends Typ[Term] with Subs[PlusTyp[U, V]] with Product with Serializable

coproduct type A + B

Self Type
PlusTyp[U, V]
Linear Supertypes
Serializable, Product, Equals, Typ[Term], Term, Subs[PlusTyp[U, V]], AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. PlusTyp
  2. Serializable
  3. Product
  4. Equals
  5. Typ
  6. Term
  7. Subs
  8. AnyRef
  9. Any
Implicitly
  1. by RichTerm
  2. by any2stringadd
  3. by StringFormat
  4. by Ensuring
  5. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new PlusTyp(first: Typ[U], second: Typ[V])

Type Members

  1. case class InducFn[W <: Term with Subs[W]](depcodom: Func[Term, Typ[W]], firstCase: FuncLike[U, W], secondCase: FuncLike[V, W]) extends InducFuncLike[Term, W] with Product with Serializable

    inductive definition on the co-product

  2. type Obj = Term

    scala type of objects with this HoTT-type (refining U)

    scala type of objects with this HoTT-type (refining U)

    Definition Classes
    PlusTyp → Typ

Value Members

  1. def !:(term: Term): Term

    checks term is of this type and returns it; useful for documentation.

    checks term is of this type and returns it; useful for documentation.

    Definition Classes
    Typ
  2. def &&[UU >: Term <: Term with Subs[UU], V <: Term with Subs[V]](that: Typ[V]): ProdTyp[UU, V]

    returns product type, mainly to use for "and" for structures

    returns product type, mainly to use for "and" for structures

    Definition Classes
    Typ
  3. def &:[UU >: Term <: Term with Subs[UU], V <: Term with Subs[V]](variable: V): SigmaTyp[V, UU]
    Definition Classes
    Typ
  4. def ++[UU >: Typ[Term] <: Typ[Term] with Subs[UU], VV <: Term with Subs[VV], V <: Typ[VV] with Subs[V]](those: V): SigmaTyp[UU, VV]

    returns Sigma-Type, mainly to use as "such that", for example a group type is this with product etc.

    returns Sigma-Type, mainly to use as "such that", for example a group type is this with product etc. dependent on this.

    Definition Classes
    Typ
  5. def ->:[W <: Term with Subs[W], UU >: Term <: Term with Subs[UU]](that: Typ[W]): FuncTyp[W, UU]

    function type: this -> that

    function type: this -> that

    Definition Classes
    Typ
  6. def :->[V <: Term with Subs[V]](that: V): Func[PlusTyp[U, V], V]

    constructor for (pure) lambda functions, see lmbda

    constructor for (pure) lambda functions, see lmbda

    Implicit
    This member is added by an implicit conversion from PlusTyp[U, V] toRichTerm[PlusTyp[U, V]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  7. def ::(name: String): Term

    symbolic object with given name

    symbolic object with given name

    Definition Classes
    Typ
  8. def :~>[V <: Term with Subs[V]](that: V): FuncLike[PlusTyp[U, V], V]

    constructor for (in general dependent) lambda functions, see lambda

    constructor for (in general dependent) lambda functions, see lambda

    Implicit
    This member is added by an implicit conversion from PlusTyp[U, V] toRichTerm[PlusTyp[U, V]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  9. def =:=(rhs: PlusTyp[U, V]): IdentityTyp[PlusTyp[U, V]]

    equality type 'term = rhs'

    equality type 'term = rhs'

    Implicit
    This member is added by an implicit conversion from PlusTyp[U, V] toRichTerm[PlusTyp[U, V]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  10. def Var(implicit factory: NameFactory): Term

    new variable from a factory.

    new variable from a factory.

    Definition Classes
    Typ
  11. def dependsOn(that: Term): Boolean

    returns whether this depends on that

    returns whether this depends on that

    Definition Classes
    Term
  12. val first: Typ[U]
  13. def i(value: U): FirstIncl[U, V]
  14. lazy val incl1: Func[U, FirstIncl[U, V]]
  15. lazy val incl2: Func[V, ScndIncl[U, V]]
  16. def indepOf(that: Term): Boolean

    returns whether this is independent of that.

    returns whether this is independent of that.

    Definition Classes
    Term
  17. def induc[W <: Term with Subs[W]](depcodom: Func[Term, Typ[W]]): FuncLike[FuncLike[U, W], FuncLike[FuncLike[V, W], FuncLike[Term, W]]]

    inductive definition on the coproduct

  18. def j(value: V): ScndIncl[U, V]
  19. def newobj: PlusTyp[U, V]

    A new object with the same type, to be used in place of a variable to avoid name clashes.

    A new object with the same type, to be used in place of a variable to avoid name clashes. Should throw exception when invoked for constants.

    Definition Classes
    PlusTyp → Subs
  20. def obj: Term

    factory for producing objects of the given type.

    factory for producing objects of the given type. can use {{innervar}} if one wants name unchanged.

    Definition Classes
    Typ
  21. def productElementNames: Iterator[String]
    Definition Classes
    Product
  22. def rec[W <: Term with Subs[W]](codom: Typ[W]): Func[Func[U, W], Func[Func[V, W], Func[Term, W]]]

    recursive definition on the co-product

  23. def refl: Refl[PlusTyp[U, V]]

    reflexivity term refl : term = term

    reflexivity term refl : term = term

    Implicit
    This member is added by an implicit conversion from PlusTyp[U, V] toRichTerm[PlusTyp[U, V]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  24. def replace(x: Term, y: Term): PlusTyp[U, V] with Subs[PlusTyp[U, V]]

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    Definition Classes
    Subs
  25. val second: Typ[V]
  26. def subs(x: Term, y: Term): PlusTyp[U, V]

    substitute x by y recursively in this.

    substitute x by y recursively in this.

    Definition Classes
    PlusTyp → Subs
  27. def sym(implicit name: sourcecode.Name): Term

    shortcut for symbolic object

    shortcut for symbolic object

    Definition Classes
    Typ
  28. def symbObj(name: AnySym): Term with Subs[Term]

    A symbolic object with this HoTT type, and with scala-type Obj

    A symbolic object with this HoTT type, and with scala-type Obj

    Definition Classes
    Typ
  29. lazy val typ: Universe

    type of a type is a universe.

    type of a type is a universe.

    Definition Classes
    PlusTyp → Typ → Term
  30. lazy val typlevel: Int
    Definition Classes
    Typ
  31. def usesVar(t: Term): Boolean

    returns whether the variable t is used as a variable in a lambda definition.

    returns whether the variable t is used as a variable in a lambda definition.

    Definition Classes
    Term
  32. def variable(name: AnySym): SymbObj[Term]

    A symbolic object with this HoTT type, and with scala-type Obj

    A symbolic object with this HoTT type, and with scala-type Obj

    Definition Classes
    PlusTyp → Typ
  33. def ||[UU >: Term <: Term with Subs[UU], V <: Term with Subs[V]](that: Typ[V]): PlusTyp[UU, V]

    returns coproduct type, mainly to use for "or".

    returns coproduct type, mainly to use for "or".

    Definition Classes
    Typ
  34. def ~>:[UU >: Term <: Term with Subs[UU], V <: Term with Subs[V]](variable: V): GenFuncTyp[V, UU]

    dependent function type (Pi-Type) define by a lambda: this depends on the variable, which hence gives a type family; note that a new variable is created and substituted in this to avoid name clashes.

    dependent function type (Pi-Type) define by a lambda: this depends on the variable, which hence gives a type family; note that a new variable is created and substituted in this to avoid name clashes.

    Definition Classes
    Typ
  35. object Elem

    Pattern for element of the given type.

    Pattern for element of the given type.

    Definition Classes
    Typ