Packages

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.

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.

Linear Supertypes
AnyRef, Any
Known Subclasses
CnstDepFuncConsShape, CnstFuncConsShape, FuncConsShape, IdShape
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConstructorShape
  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: Typ[H]): Typ[ConstructorType]

    returns HoTT type of the introduction rule given the (inductive) type W (to be the head).

  2. abstract val introArgs: Int
  3. abstract def mapper[Cod <: Term with Subs[Cod]]: ConstructorPatternMapper[S, Cod, ConstructorType, H, RecDataType, InducDataType] forSome {type RecDataType <: Term with Subs[RecDataType], type InducDataType <: Term with Subs[InducDataType]}

    helper to give ConstructorPatternMap when scala type of codomain is specified.

  4. abstract def subs(x: Term, y: Term): ConstructorShape[S, H, ConstructorType]

Concrete Value Members

  1. def -->:(that: IdShape.type): FuncConsShape[S, H, ConstructorType, H]

    returns shape that -> this' where that must be the shape for inductive type W

  2. def -->:[F <: Term with Subs[F]](that: IterFuncShape[H, F]): FuncConsShape[S, H, ConstructorType, F]

    returns shape that -> this' where that is of the form W, A -> W etc; invoking this is an error if we that is independent of W

  3. def ->:[T <: Term with Subs[T]](tail: Typ[T]): CnstFuncConsShape[S, H, ConstructorType, T, Nothing]

    returns shape tail ->: this where tail must be independent of the inductive type W being defined.

  4. def lift[Cod <: Term with Subs[Cod], RecDataType <: Term with Subs[RecDataType], InducDataType <: Term with Subs[InducDataType]](implicit mp: ConstructorPatternMapper[S, Cod, ConstructorType, H, RecDataType, InducDataType]): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]

    lift to ConstructorPatternMap using an implicit ConstructorPatternMapper, which could from the mapper method.

  5. def mapped[Cod <: Term with Subs[Cod]]: ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] forSome {type RecDataType <: Term with Subs[RecDataType], type InducDataType <: Term with Subs[InducDataType]}

    lift to ConstructorPatternMap using the result of the mapper method.

  6. def symbcons(name: AnySym, tp: Typ[H]): symbcons._1.type.Obj with Subs[symbcons._1.type.Obj] forSome {val _1: Typ[ConstructorType]}

    returns term giving introduction rule given inductive type and name

  7. def ~>:[T <: Term with Subs[T]](tailVar: T): CnstDepFuncConsShape[S, H, ConstructorType, T, Nothing]

    returns dependent shape tail ~>: this where tail must be independent of the inductive type W being defined.