Packages

sealed abstract class IndexedConstructorPatternMap[Cod <: Term with Subs[Cod], ConstructorType <: Term with Subs[ConstructorType], H <: Term with Subs[H], RecDataType <: Term with Subs[RecDataType], InducDataType <: Term with Subs[InducDataType], Fb <: Term with Subs[Fb], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

Introduction rule for an indexed inductive type, as in IndexedConstructorShape with the scala type of the codomain specified; hence the scala type of the recurion and induction types are determined. The definitions of recursion and induction functions for the case matching the introduction rule are the abstract methods recDefCase and inducDefCase.

Cod

the scala type of the codomain.

ConstructorType

the scala type of the introduction rule

H

the scala type of terms of an inductive type that can have this constructor.

RecDataType

type of data for recursive definitions for the case corresponding to this introduction rule.

InducDataType

type of data for inductive definitions for the case corresponding to this introduction rule.

Fb

scala type of the inductive type family

Index

scala type of the index

IF

scala type of an iterated function on the inductive type family, with codomain with terms of type Cod.

IDF

scala type of an iterated dependent function on the inductive type family, with codomain with terms of type Cod.

IDFT

scala type of an iterated type family on the inductive type family, i.e., with codomain with terms of type Typ[Cod] this is used indirectly through IndexedConstructorSeqMap

Self Type
IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
Linear Supertypes
AnyRef, Any
Known Subclasses
IndexedCnstDepFncPtnMap, IndexedCnstFncPtnMap, IndexedFuncPtnMap, IndexedIdMap, IndexedIndexedFuncPtnMap, IndexedRecursiveConstructorPatternMap
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IndexedConstructorPatternMap
  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: TypFamilyMap[H, Fb, Cod, Index, IF, IDF, IDFT]

    the inductive type family

  3. abstract def inducDataTyp(w: Fb, xs: IDFT)(cons: ConstructorType): Typ[InducDataType]

    domain containing the induction data for the constructor, i.e., the HoTT type of the induction data.

  4. abstract def inducDefCase(cons: ConstructorType, data: InducDataType, f: => IDF): (H) => Option[Cod]

    given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.

    given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern. optionally returns simplification (if the term matches).

    cons

    constructor, actually quasi-constructor, with which to match.

    data

    definition data for the image of the constructor.

    f

    the function being defined inductively, to be used recursively in definition.

  5. abstract def recDataTyp(wb: Fb, x: Typ[Cod]): Typ[RecDataType]

    domain containing the recursion data for the constructor, i.e., the HoTT type of recursion data.

  6. abstract def recDefCase(cons: ConstructorType, data: RecDataType, f: => IF): (H) => Option[Cod]

    given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.

    given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern. optionally returns simplification (if the term matches), determined by the recursion data.

    cons

    constructor, actually quasi-constructor, with which to match.

    data

    definition data for the image of the constructor.

    f

    the function being defined recursively, to be used recursively in definition.

  7. abstract def subs(x: Term, y: Term): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
  8. abstract val univLevel: Int