Packages

case class ConstructorSeqTL[SS <: HList, H <: Term with Subs[H], Intros <: HList](seqDom: ConstructorSeqDom[SS, H, Intros], typ: Typ[H]) extends Product with Serializable

Essentially the definition of an inductive type; has all parameters of the definition:

SS

shape sequence - a formal type for lifting information about introduction rules to type level.

H

the scala type of terms in the inductive type typ

Intros

the scala type of the introduction rules We can define functions recursively using the rec method and inductively using the induc method.

seqDom

the sequence of introduction rules.

typ

the inductive type being defined.

Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConstructorSeqTL
  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 ConstructorSeqTL(seqDom: ConstructorSeqDom[SS, H, Intros], typ: Typ[H])

    seqDom

    the sequence of introduction rules.

    typ

    the inductive type being defined.

Value Members

  1. def induc[C <: Term with Subs[C], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](Xs: Func[H, Typ[C]])(implicit mapper: ConstructorSeqMapper[SS, C, H, RecType, InducType, Intros]): InducType

    returns the term ind_W, X for inductively defining function to the type family Xs on W from the inductive type W = typ; an implicit mapper is used, which also allows calculation of the type RecType.

    returns the term ind_W, X for inductively defining function to the type family Xs on W from the inductive type W = typ; an implicit mapper is used, which also allows calculation of the type RecType.

    RecType

    not used here, but part of the definition of the mapper.

    InducType

    the type of the induc function returned.

  2. def inducE[C <: Term with Subs[C]](Xs: Func[H, Typ[C]]): InducType forSome {type InducType <: Term with Subs[InducType]}

    Existential typed version of induc to be used at runtime if necessary.

  3. val intros: Intros

    The introduction rules.

  4. def productElementNames: Iterator[String]
    Definition Classes
    Product
  5. def rec[C <: Term with Subs[C], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](X: Typ[C])(implicit mapper: ConstructorSeqMapper[SS, C, H, RecType, InducType, Intros]): RecType

    returns the term rec_W, X for recursively defining function to X from the inductive type W = typ; an implicit mapper is used, which also allows calculation of the type RecType.

    returns the term rec_W, X for recursively defining function to X from the inductive type W = typ; an implicit mapper is used, which also allows calculation of the type RecType.

    RecType

    type of the rec function returned;

    InducType

    not used here, but part of the definition of the mapper.

    X

    the codomain to which we wish to define recursive functions - the only one we need to specify;

  6. def recE[C <: Term with Subs[C]](X: Typ[C]): RecType forSome {type RecType <: Term with Subs[RecType]}

    Existential typed version of rec for use at runtime if neccesary.

  7. val seqDom: ConstructorSeqDom[SS, H, Intros]
  8. def subs(x: Term, y: Term): ConstructorSeqTL[SS, H, Intros]
  9. val typ: Typ[H]
  10. def |:[S <: HList, ConstructorType <: Term with Subs[ConstructorType]](head: ConstructorTL[S, H, ConstructorType]): ConstructorSeqTL[::[S, SS], H, ::[ConstructorType, Intros]]

    Prepend to the sequence of introduction rules.