Type Members

1.  sealed trait ConstructorPatternMap[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]] extends AnyRef

   Introduction rule for an inductive type, as in ConstructorShape with the scala type of the codomain specified; hence the scala type of the recurion and induction types are determined.

   Introduction rule for an inductive type, as in ConstructorShape 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. this is used indirectly through ConstructorSeqTL

2.  sealed trait ConstructorPatternMapper[Shape <: HList, 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]] extends AnyRef

   bridge between the definition ConstructorShape of an introduction rule and ConstructorPatternMap which depends also on the scala type of the codomain, allowing cases for recursive and inductive definition; ideally used implicitly.

3.  sealed trait ConstructorSeqDom[SS <: HList, H <: Term with Subs[H], Intros <: HList] extends AnyRef

   the shape of the definition of an inductive type; when a type is specified we get an object of type ConstructorSeqTL, which is the full definition

   the shape of the definition of an inductive type; when a type is specified we get an object of type ConstructorSeqTL, which is the full definition

   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

4.  sealed trait ConstructorSeqMap[C <: Term with Subs[C], H <: Term with Subs[H], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType], Intros <: HList] extends AnyRef

   Inductive type definition as in ConstructorSeqTL together with the scala type of a codomain; this determines the scala type of rec_W,X and induc_W, Xs functions.

   Inductive type definition as in ConstructorSeqTL together with the scala type of a codomain; this determines the scala type of rec_W,X and induc_W, Xs functions. methods return recursive and inductive definitions for a given codomain; these are lambda forms of definitions made for each introduction rule in ConstructorPatternMap and combined for different introduction rules in RecursiveDefinition and InductiveDefinition

   C

   scala type of terms in the codomain for defining recursive/inductive function

   H

   scala type of terms in the inductive type with this shape.

   RecType

   scala type of a function rec_W, X

   InducType

   scala type of a function ind_W, X

   Intros

   introduction rules for inductive type of this shape

5.  sealed trait ConstructorSeqMapper[SS <: HList, C <: Term with Subs[C], H <: Term with Subs[H], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType], Intros <: HList] extends AnyRef

   given scala type of the codomain and a specific inductive type, lifts a ConstructorSeqDom to a ConstructorSeqMap

6.  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:

   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.

7.  sealed trait ConstructorShape[S <: HList, H <: Term with Subs[H], ConstructorType <: Term with Subs[ConstructorType]] extends AnyRef

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

   The introduction rule for an inductive type, as a function of the type; typically (A -> B -> W)-> C -> W -> (D -> W) -> W 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.

   ConstructorType

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

8.  case class ConstructorTL[S <: HList, H <: Term with Subs[H], ConstructorType <: Term with Subs[ConstructorType]](name: AnySym, shape: ConstructorShape[S, H, ConstructorType], W: Typ[H]) extends Product with Serializable

   an introduction rule for an inductive type

9.  case class ConstructorTypTL[S <: HList, H <: Term with Subs[H], ConstructorType <: Term with Subs[ConstructorType]](shape: ConstructorShape[S, H, ConstructorType], typ: Typ[H]) extends Product with Serializable

   an introduction rule shape together with the iductive type typ being defined.

10.  case class ExstInducDefn(typFamily: Term, intros: Vector[Term], ind: ExstInducStrucs) extends Product with Serializable
11.  trait ExstInducStrucs extends AnyRef

    term level inductive structures for runtime contexts

12.  case class IndTyp[SS <: HList, Intros <: HList](name: String, seqDom: ConstructorSeqDom[SS, Term, Intros]) extends Typ[Term] with Product with Serializable
13.  case class IndexedConstructor[S <: HList, H <: Term with Subs[H], F <: Term with Subs[F], ConstructorType <: Term with Subs[ConstructorType], Index <: HList](name: AnySym, shape: IndexedConstructorShape[S, H, F, ConstructorType, Index])(implicit evidence$21: TermList[Index]) extends Product with Serializable
14.  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.

    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

15.  sealed abstract class IndexedConstructorPatternMapper[S <: HList, 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], F <: Term with Subs[F], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    bridge between IndexedConstructorShape and IndexedConstructorPatternMap

16.  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;

    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

17.  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.

    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]

18.  sealed abstract class IndexedConstructorSeqMapper[SS <: HList, 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

    bride between IndexedConstructorSeqDom and IndexedConstructorSeqMap

19.  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.

    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

20.  sealed abstract class IndexedInductiveDefinition[H <: Term with Subs[H], F <: Term with Subs[F], C <: Term with Subs[C], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    indexed version of InductiveDefinition

21.  sealed abstract class IndexedIterFuncPtnMap[H <: Term with Subs[H], Fb <: Term with Subs[Fb], Index <: HList, C <: Term with Subs[C], F <: Term with Subs[F], TT <: Term with Subs[TT], DT <: Term with Subs[DT], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    Indexed version of IterFuncPtnMap

22.  sealed abstract class IndexedIterFuncPtnMapper[H <: Term with Subs[H], Fb <: Term with Subs[Fb], Index <: HList, C <: Term with Subs[C], F <: Term with Subs[F], TT <: Term with Subs[TT], DT <: Term with Subs[DT], IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    bridge between IndexedIterFuncShape and IndexedIterFuncPtnMap

23.  sealed abstract class IndexedIterFuncShape[H <: Term with Subs[H], F <: Term with Subs[F], Fb <: Term with Subs[Fb], Index <: HList] extends AnyRef

    indexed version of IterFuncShape

24.  sealed abstract class IndexedRecursiveDefinition[H <: Term with Subs[H], F <: Term with Subs[F], C <: Term with Subs[C], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    indexed version of RecursiveDefinition

25.  trait InductionImplicits extends AnyRef
26.  sealed trait InductiveDefinition[H <: Term with Subs[H], C <: Term with Subs[C]] extends InducFuncLike[H, C]

    inductively defined dependent function, to be built by mixing in cases, defaults to a formal application by itself

27.  sealed trait IterFuncMapper[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F], TT <: Term with Subs[TT], DT <: Term with Subs[DT]] extends AnyRef

    Given the scala type of the codomain, lifts IterFuncShape to IterFuncMapper

28.  sealed trait IterFuncPtnMap[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F], TT <: Term with Subs[TT], DT <: Term with Subs[DT]] extends AnyRef

    a family of the form P: A -> B -> W etc, or dependent versions of this as a function of W, together with the scala type of a codomain; has methods for defining induced functions and dependent functions.

    a family of the form P: A -> B -> W etc, or dependent versions of this as a function of W, together with the scala type of a codomain; has methods for defining induced functions and dependent functions.

    O

    scala type of terms of the type W

    C

    scala type of codomain

    F

    scala type of the family eg P: A -> W

    TT

    scala type of family type eg A -> B -> X, ie, codomain of induced function

    DT

    scala type of family type eg A -> B -> X, ie, codomain of induced function

29.  sealed trait IterFuncShape[O <: Term with Subs[O], F <: Term with Subs[F]] extends AnyRef

    a family of the form P: A -> B -> W etc, or dependent versions of this as a function of W.

    a family of the form P: A -> B -> W etc, or dependent versions of this as a function of W.

    O

    scala type of terms of the type W

    F

    scala type of the family eg P: A -> W

30.  case class NoIntro(w: Typ[Term], cnstTyp: Typ[Term]) extends Exception with Product with Serializable
31.  case class NotFunc(t: Term) extends Exception with Product with Serializable
32.  trait RecursiveDefinition[H <: Term with Subs[H], C <: Term with Subs[C]] extends RecFunc[H, C]

    recursively defined function, to be built by mixing in cases, defaults to a formal application by itself

33.  sealed trait TypFamilyExst extends AnyRef
34.  abstract class TypFamilyMap[H <: Term with Subs[H], F <: Term with Subs[F], C <: Term with Subs[C], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    shape of a type family, together with the type of a codomain; fixing scala types of functions and dependent functions on the type family

    shape of a type family, together with the type of a codomain; fixing scala types of functions and dependent functions on the 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] methods allow restricting (dependent) functions and type families to indices and building (dependent) functions from such restrictions.

35.  abstract class TypFamilyMapper[H <: Term with Subs[H], F <: Term with Subs[F], C <: Term with Subs[C], Index <: HList, IF <: Term with Subs[IF], IDF <: Term with Subs[IDF], IDFT <: Term with Subs[IDFT]] extends AnyRef

    bridge between TypFamilyPtn and TypFamilyMap

36.  sealed abstract class TypFamilyPtn[H <: Term with Subs[H], F <: Term with Subs[F], Index <: HList] extends AnyRef

    the shape of a type family.

37.  trait TypFamilyPtnGetter[F <: Term with Subs[F], H <: Term with Subs[H], Index <: HList] extends AnyRef
38.  class TypObj[T <: Typ[Term] with Subs[T], C <: Term with Subs[C]] extends AnyRef

    aid for implicit calculations: given a scala type that is a subtype of Typ[C], recovers C, eg shows that FuncTyp[A, B] is a subtype of Typ[Func[A, B]]

    aid for implicit calculations: given a scala type that is a subtype of Typ[C], recovers C, eg shows that FuncTyp[A, B] is a subtype of Typ[Func[A, B]]

    Note that C is not unique, indeed C = Term is always a solution, so we seek the best C

39.  trait WeakImplicit extends AnyRef