ConstructorPatternMap

Companion object ConstructorPatternMap

sealed trait ConstructorPatternMap[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]] extends AnyRef

Introduction rule for an inductive type, as in ConstructorShape 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. this is used indirectly through ConstructorSeqTL

Self Type: ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]

Linear Supertypes

AnyRef, Any

Known Subclasses

CnstDepFuncPtnMap, CnstFncPtnMap, FuncPtnMap, IdTargMap, RecursiveConstructorPatternMap

Type Hierarchy

Ordering

Alphabetic
By Inheritance

Inherited

ConstructorPatternMap
AnyRef
Any

Implicitly

by any2stringadd
by StringFormat
by Ensuring
by ArrowAssoc

Hide All
Show All

Visibility

Public
Protected

Abstract Value Members

abstract def codFromData(d: RecDataType): Typ[Cod]
abstract def inducDataTyp(w: Typ[H], xs: Func[H, Typ[Cod]])(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: => FuncLike[H, Cod]): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor 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(w: Typ[H], 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: => Func[H, Cod]): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor 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): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
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 ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toany2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method any2stringadd in scala.Predef.
Definition Classes
any2stringadd
def ->[B](y: B): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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 ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toStringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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.

Inherited from AnyRef

Value Members

final def !=(arg0: Any): Boolean
Definition Classes
AnyRef → Any
final def ##: Int
Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean
Definition Classes
AnyRef → Any
def clone(): AnyRef
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
final def eq(arg0: AnyRef): Boolean
Definition Classes
AnyRef
def equals(arg0: AnyRef): Boolean
Definition Classes
AnyRef → Any
final def getClass(): Class[_ <: AnyRef]
Definition Classes
AnyRef → Any
Annotations
@native() @HotSpotIntrinsicCandidate()
def hashCode(): Int
Definition Classes
AnyRef → Any
Annotations
@native() @HotSpotIntrinsicCandidate()
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])
def finalize(): Unit
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.Throwable]) @Deprecated
Deprecated

Inherited from Any

Value Members

final def asInstanceOf[T0]: T0
Definition Classes
Any
final def isInstanceOf[T0]: Boolean
Definition Classes
Any

Inherited by implicit conversion any2stringadd fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to any2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

def +(other: String): String
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toany2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method any2stringadd in scala.Predef.
Definition Classes
any2stringadd

Inherited by implicit conversion StringFormat fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to StringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

def formatted(fmtstr: String): String
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toStringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method StringFormat in scala.Predef.
Definition Classes
StringFormat
Annotations
@inline()

Inherited by implicit conversion Ensuring fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to Ensuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

def ensuring(cond: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring

Inherited by implicit conversion ArrowAssoc fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to ArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

def ->[B](y: B): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method ArrowAssoc in scala.Predef.
Definition Classes
ArrowAssoc
Annotations
@inline()
def →[B](y: B): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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.

Ungrouped

abstract def codFromData(d: RecDataType): Typ[Cod]
abstract def inducDataTyp(w: Typ[H], xs: Func[H, Typ[Cod]])(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: => FuncLike[H, Cod]): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor 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(w: Typ[H], 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: => Func[H, Cod]): (H) => Option[Cod]
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor pattern.
given a term, matches to see if this is the image of a given (quasi)-constructor, with this constructor 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): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
abstract val univLevel: Int
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 ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toany2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method any2stringadd in scala.Predef.
Definition Classes
any2stringadd
def ->[B](y: B): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]) => Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean, msg: => Any): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean): ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toEnsuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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 ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toStringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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])
def finalize(): Unit
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.Throwable]) @Deprecated
Deprecated
def →[B](y: B): (ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType], B)
Implicit
This member is added by an implicit conversion from ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] toArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]] 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.

Packages

Inductive Type Definitions

Recursion and Induction functions

Indexed Versions

ConstructorPatternMap

Companion object ConstructorPatternMap

sealed trait ConstructorPatternMap[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]] extends AnyRef

Abstract Value Members

Concrete Value Members

Deprecated Value Members

Inherited from AnyRef

Value Members

Inherited from Any

Value Members

Inherited by implicit conversion any2stringadd fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to any2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion StringFormat fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to StringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion Ensuring fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to Ensuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion ArrowAssoc fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to ArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Ungrouped

Packages

Inductive Type Definitions

Recursion and Induction functions

Indexed Versions

ConstructorPatternMap

Companion object ConstructorPatternMap

sealed trait ConstructorPatternMap[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]] extends AnyRef

Abstract Value Members

Concrete Value Members

Deprecated Value Members

Inherited from AnyRef

Value Members

Inherited from Any

Value Members

Inherited by implicit conversion any2stringadd fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to any2stringadd[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion StringFormat fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to StringFormat[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion Ensuring fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to Ensuring[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Inherited by implicit conversion ArrowAssoc fromConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType] to ArrowAssoc[ConstructorPatternMap[Cod, ConstructorType, H, RecDataType, InducDataType]]

Value Members

Ungrouped

ConstructorPatternMap