Packages

object ConstructorSeqMap

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConstructorSeqMap
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class Cons[C <: Term with Subs[C], H <: Term with Subs[H], Cod <: Term with Subs[Cod], RD <: Term with Subs[RD], ID <: Term with Subs[ID], TR <: Term with Subs[TR], TI <: Term with Subs[TI], TIntros <: HList](cons: C, pattern: ConstructorPatternMap[Cod, C, H, RD, ID], tail: ConstructorSeqMap[Cod, H, TR, TI, TIntros]) extends ConstructorSeqMap[Cod, H, Func[RD, TR], Func[ID, TI], ::[C, TIntros]] with Product with Serializable

    prepending an introduction rule to ConstructorSeqMap

    prepending an introduction rule to ConstructorSeqMap

    cons

    the introduction rule

    pattern

    the mapped version of the introduction rule for the given codomain

    tail

    the tail ConstructorSeqMap

  2. case class ConsIndException[C <: Term with Subs[C], H <: Term with Subs[H], Cod <: Term with Subs[Cod], RD <: Term with Subs[RD], ID <: Term with Subs[ID], TR <: Term with Subs[TR], TI <: Term with Subs[TI], TIntros <: HList](cons: Cons[C, H, Cod, RD, ID, TR, TI, TIntros], fibre: Func[H, Typ[Cod]], error: Throwable) extends Exception with Product with Serializable
  3. case class Empty[C <: Term with Subs[C], H <: Term with Subs[H]](W: Typ[H]) extends ConstructorSeqMap[C, H, Func[H, C], FuncLike[H, C], HNil] with Product with Serializable

    ConstructorSeqMap for an empty sequence of introduction rules

  4. case class InducDataSym[C <: Term with Subs[C]](cons: C) extends AnySym with Product with Serializable

    formal symbol for definition data for an induction symbol

  5. case class RecDataSym[C <: Term with Subs[C]](cons: C) extends AnySym with Product with Serializable

    formal symbol for definition data for a recursion function