Packages

sealed abstract class IndexedConstructorShape[S <: HList, H <: Term with Subs[H], Fb <: Term with Subs[Fb], ConstructorType <: Term with Subs[ConstructorType], Index <: HList] extends AnyRef

The introduction rule for an indexed inductive type; typically (A -> B -> W(x))-> C -> W(y) -> (D -> W(y)) -> W(z) as a function of W May have Pi-types instead of function types.

Usually constructed using the DSL in TLImplicits

S

formal type to capture information at type level

H

scala type of the terms of the inductive type.

Fb

scala type of the inudctive type family

ConstructorType

scala type of a constructor (introduction rule) corresponding to this pattern.

Index

scala type of the index

Linear Supertypes
AnyRef, Any
Known Subclasses
IndexedCnstDepFuncConsShape, IndexedCnstFuncConsShape, IndexedIdShape, IndexedIndexedFuncConsShape, IndexedFuncConsShape
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IndexedConstructorShape
  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 def apply(tp: Fb): Typ[ConstructorType]

    returns HoTT type corresponding to the pattern given the (inductive) type family W (to be the head).

  2. abstract val family: TypFamilyPtn[H, Fb, Index]
  3. abstract def mapper[C <: Term with Subs[C], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]](implicit fmlyMapper: TypFamilyMapper[H, Fb, C, Index, IF, IDF, IDFT]): IndexedConstructorPatternMapper[S, C, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] forSome {type RecDataType <: Term with Subs[RecDataType], type InducDataType <: Term with Subs[InducDataType]}

    helper to give ConstructorPatternMap when scala type of codomain is specified.

  4. abstract def subs(x: Term, y: Term): IndexedConstructorShape[S, H, Fb, ConstructorType, Index]

Concrete Value Members

  1. def -->>:[F <: Term with Subs[F]](that: IndexedIterFuncShape[H, F, Fb, Index], ind: Index): IndexedIndexedFuncConsShape[S, H, F, ConstructorType, Fb, Index]

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

  2. def ->>:[T <: Term with Subs[T]](tail: Typ[T]): IndexedCnstFuncConsShape[S, T, H, Fb, ConstructorType, Index]

    returns shape tail ->: this where tail must be independent of the inductive type W being defined.

  3. def :::(name: AnySym): IndexedConstructor[S, H, Fb, ConstructorType, Index]

    returns a variable to act as an introduction rule.

  4. 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, Fb, C, Index, IF, IDF, IDFT]): IndexedConstructorPatternMap[C, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] forSome {type RecDataType <: Term with Subs[RecDataType], type InducDataType <: Term with Subs[InducDataType]}

    lift to IndexedConstructorPatternMap using the result of the mapper method.

  5. def symbcons(name: AnySym, tp: Fb): ConstructorType

    returns term giving introduction rule given inductive type and name

  6. def ~>>:[T <: Term with Subs[T]](tailVar: T): IndexedCnstDepFuncConsShape[S, T, H, Fb, ConstructorType, Index]

    returns dependent shape tail ~>: this where tail must be independent of the inductive type W being defined.