Packages

sealed abstract class IndexedConstructorSeqDom[SS <: HList, H <: Term with Subs[H], F <: Term with Subs[F], Index <: HList, Intros <: HList] extends AnyRef

Essentially the definition of an indexed inductive type;

SS

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

H

the scala type of terms in an inductive type of this shape

Intros

the scala type of the introduction rules

Linear Supertypes
AnyRef, Any
Known Subclasses
Cons, Empty
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IndexedConstructorSeqDom
  2. AnyRef
  3. 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

Abstract Value Members

  1. abstract val W: F

    the inductive type family

  2. abstract val family: TypFamilyPtn[H, F, Index]

    the index family

  3. abstract val intros: Intros

    the introduction rules

  4. abstract def mapped[C <: Term with Subs[C], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]](implicit fmlyMapper: TypFamilyMapper[H, F, C, Index, IF, IDF, IDFT]): IndexedConstructorSeqMap[C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT] forSome {type RecType <: Term with Subs[RecType], type InducType <: Term with Subs[InducType]}

    existentitally typed lift given codomain

  5. abstract def subs(x: Term, y: Term): IndexedConstructorSeqDom[SS, H, F, Index, Intros]

Concrete Value Members

  1. def getInduc[C <: Term with Subs[C], IDFT <: Term with Subs[IDFT], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](X: Typ[C])(implicit mapper: IndexedConstructorSeqMapper[SS, C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]): (IDFT) => InducType
  2. def getMapper[C <: Term with Subs[C], IDFT <: Term with Subs[IDFT], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](X: Typ[C])(implicit mapper: IndexedConstructorSeqMapper[SS, C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]): IndexedConstructorSeqMap[C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]
  3. def induc[IDFT <: Term with Subs[IDFT], C <: Term with Subs[C], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](Xs: IDFT)(implicit mapper: IndexedConstructorSeqMapper[SS, C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]): InducType

    induction function based on implicits

  4. def inducE[IDFT <: Term with Subs[IDFT]](Xs: IDFT): InducType forSome {type InducType <: Term with Subs[InducType]}

    existentitally typed induction function

  5. def rec[C <: Term with Subs[C], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](X: Typ[C])(implicit mapper: IndexedConstructorSeqMapper[SS, C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]): RecType

    recursion function definition based on implcits

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

    existentitally typed recursion function definition

  7. def |:[HShape <: HList, HC <: Term with Subs[HC]](head: IndexedConstructor[HShape, H, F, HC, Index]): IndexedConstructorSeqDom[::[HShape, SS], H, F, Index, ::[HC, Intros]]

    prepend introduction rule