Packages

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

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. ConstructorSeqDom
  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 introArgsVec: Vector[Int]
  2. abstract def intros(typ: Typ[H]): Intros

    returns introduction rules, given an inductive type.

  3. abstract def mapped[C <: Term with Subs[C]](W: Typ[H]): ConstructorSeqMap[C, H, RecType, InducType, TIntros] forSome {type RecType <: Term with Subs[RecType], type InducType <: Term with Subs[InducType], type TIntros <: HList}

    given a codomain, returns a mapped version, i.e.

    given a codomain, returns a mapped version, i.e. one with all the types needed for recursion and induction.

  4. abstract val numIntros: Int
  5. abstract def subs(x: Term, y: Term): ConstructorSeqDom[SS, H, Intros]

Concrete Value Members

  1. def induc[C <: Term with Subs[C]](W: Typ[H], Xs: Func[H, Typ[C]]): InducType forSome {type InducType <: Term with Subs[InducType]}

    existential typed ind_W, X, used by the method indE of ConstructorSeqTL

  2. def rec[C <: Term with Subs[C]](W: Typ[H], X: Typ[C]): RecType forSome {type RecType <: Term with Subs[RecType]}

    existential typed rec_W, X, used by the method recE of ConstructorSeqTL