Packages

case class ConstructorTypTL[S <: HList, H <: Term with Subs[H], ConstructorType <: Term with Subs[ConstructorType]](shape: ConstructorShape[S, H, ConstructorType], typ: Typ[H]) extends Product with Serializable

an introduction rule shape together with the iductive type typ being defined.

Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConstructorTypTL
  2. Serializable
  3. Product
  4. Equals
  5. AnyRef
  6. 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

Instance Constructors

  1. new ConstructorTypTL(shape: ConstructorShape[S, H, ConstructorType], typ: Typ[H])

Value Members

  1. def -->>:[F <: Term with Subs[F]](that: IterFuncShape[H, F]): ConstructorTypTL[::[FuncConsShape.type, S], H, Func[F, ConstructorType]]

    returns constructor with shape that -> this' where that is of the form W, A -> W etc; invoking this is an error if we that is independent of W

  2. def -->>:(that: Typ[H]): ConstructorTypTL[::[FuncConsShape.type, S], H, Func[H, ConstructorType]]

    returns constructor with shape W -> this'; invoking this is an error if we that is not W

  3. def ->>:[T <: Term with Subs[T]](that: Typ[T]): ConstructorTypTL[::[CnstFuncConsShape.type, S], H, Func[T, ConstructorType]]

    returns constructor with shape that -> this' where that is a type A; invoking this is an error if we that is not independent of W

  4. def :::(name: AnySym): ConstructorTL[S, H, ConstructorType]

    returns a variable to act as an introduction rule.

  5. def productElementNames: Iterator[String]
    Definition Classes
    Product
  6. val shape: ConstructorShape[S, H, ConstructorType]
  7. val typ: Typ[H]
  8. def ~>>:(thatVar: H): ConstructorTypTL[::[CnstDepFuncConsShape.type, S], H, FuncLike[H, ConstructorType]]

    returns constructor with shape that ~> this' where that is a type A; invoking this is an error if we that is not independent of W