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. 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
- Self Type
- IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- Alphabetic
- By Inheritance
- IndexedConstructorPatternMap
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Abstract Value Members
- abstract def apply(tp: Fb): Typ[ConstructorType]
returns HoTT type corresponding to the pattern given the (inductive) type family W (to be the head).
- abstract val family: TypFamilyMap[H, Fb, Cod, Index, IF, IDF, IDFT]
the inductive type family
- abstract def inducDataTyp(w: Fb, xs: IDFT)(cons: ConstructorType): Typ[InducDataType]
domain containing the induction data for the constructor, i.e., the HoTT type of the induction data.
- abstract def inducDefCase(cons: ConstructorType, data: InducDataType, f: => IDF): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with
thisconstructor pattern.given a term, matches to see if this is the image of a given (quasi)-constructor, with
thisconstructor pattern. optionally returns simplification (if the term matches).- cons
constructor, actually quasi-constructor, with which to match.
- data
definition data for the image of the constructor.
- f
the function being defined inductively, to be used recursively in definition.
- abstract def recDataTyp(wb: Fb, x: Typ[Cod]): Typ[RecDataType]
domain containing the recursion data for the constructor, i.e., the HoTT type of recursion data.
- abstract def recDefCase(cons: ConstructorType, data: RecDataType, f: => IF): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with
thisconstructor pattern.given a term, matches to see if this is the image of a given (quasi)-constructor, with
thisconstructor pattern. optionally returns simplification (if the term matches), determined by the recursion data.- cons
constructor, actually quasi-constructor, with which to match.
- data
definition data for the image of the constructor.
- f
the function being defined recursively, to be used recursively in definition.
- abstract def subs(x: Term, y: Term): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- abstract val univLevel: Int
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toany2stringadd[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
- def ->[B](y: B): (IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT], B)
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toArrowAssoc[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- def ensuring(cond: (IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]) => Boolean, msg: => Any): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toEnsuring[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]) => Boolean): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toEnsuring[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toEnsuring[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toEnsuring[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toStringFormat[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @inline()
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def →[B](y: B): (IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT], B)
- Implicit
- This member is added by an implicit conversion from IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT] toArrowAssoc[IndexedConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType, Fb, Index, IF, IDF, IDFT]] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.