Packages

sealed abstract class IndexedConstructorSeqMap[C <: Term with Subs[C], H <: Term with Subs[H], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType], Intros <: HList, F <: Term with Subs[F], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

indexed version of ConstructorSeqMap, giving definitions of indexed recursion and induction functions.

H

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

RecType

scala type of the recursion function

InducType

scala type of the induction function

Intros

scala type of the introduction rules

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]

Linear Supertypes
AnyRef, Any
Known Subclasses
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IndexedConstructorSeqMap
  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 index type family

  2. abstract val family: TypFamilyMap[H, F, C, Index, IF, IDF, IDFT]

    the inductive type family

  3. abstract def inducDataLambda(fibre: IDFT): (IDF) => InducType
  4. abstract def inducDefn(fibre: IDFT): IndexedInductiveDefinition[H, F, C, Index, IF, IDF, IDFT]

    the raw inductive definition, from which the induction function is built by lambdas

  5. abstract def recDataLambda(X: Typ[C]): (IF) => RecType
  6. abstract def recDefn(X: Typ[C]): IndexedRecursiveDefinition[H, F, C, Index, IF, IDF, IDFT]

    the raw recursive definition, from which the recursion function is built by lambdas

  7. abstract def subs(x: Term, y: Term): IndexedConstructorSeqMap[C, H, RecType, InducType, Intros, F, Index, IF, IDF, IDFT]

Concrete Value Members

  1. def induc(fibre: IDFT): InducType

    the induction function

  2. def inducF(fibre: Term): InducType

    the induction function with type casting

  3. def rec(X: Typ[C]): RecType

    the recursion function