Packages

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

Linear Supertypes
AnyRef, Any
Known Subclasses
Cons, Empty
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConstructorSeqMap
  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: Typ[H]

    the inductive type being defined

  2. abstract def inducDataLambda(fibre: Func[H, Typ[C]]): (FuncLike[H, C]) => InducType

    converts an inductive definition built by InductiveDefinition to a lambda

  3. abstract def inducDefn(fibre: Func[H, Typ[C]]): InductiveDefinition[H, C]

    inductive definition function ind_W, X in raw form

  4. abstract def recDataLambda(X: Typ[C]): (Func[H, C]) => RecType

    converts a recursive definition built by RecursiveDefinition to a lambda

  5. abstract def recDefn(X: Typ[C]): RecursiveDefinition[H, C]

    recursive definition function rec_W, X in raw form

  6. abstract def subs(x: Term, y: Term): ConstructorSeqMap[C, H, RecType, InducType, Intros]

Concrete Value Members

  1. def induc(fibre: Func[H, Typ[C]]): InducType

    inductive definition function ind_W, Xs

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

    the recursion function rec_W,X