case class ConstructorSeqTL[SS <: HList, H <: Term with Subs[H], Intros <: HList](seqDom: ConstructorSeqDom[SS, H, Intros], typ: Typ[H]) extends Product with Serializable
Essentially the definition of an inductive type; has all parameters of the definition:
- SS
shape sequence- H
the scala type of terms in the inductive type
typ- Intros
the scala type of the introduction rules We can define functions recursively using the rec method and inductively using the induc method.
- seqDom
the sequence of introduction rules.
- typ
the inductive type being defined.
- Alphabetic
- By Inheritance
- ConstructorSeqTL
- Serializable
- Product
- Equals
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new ConstructorSeqTL(seqDom: ConstructorSeqDom[SS, H, Intros], typ: Typ[H])
- seqDom
the sequence of introduction rules.
- typ
the inductive type being defined.
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 ConstructorSeqTL[SS, H, Intros] toany2stringadd[ConstructorSeqTL[SS, H, Intros]] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
- def ->[B](y: B): (ConstructorSeqTL[SS, H, Intros], B)
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toArrowAssoc[ConstructorSeqTL[SS, H, Intros]] 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: (ConstructorSeqTL[SS, H, Intros]) => Boolean, msg: => Any): ConstructorSeqTL[SS, H, Intros]
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toEnsuring[ConstructorSeqTL[SS, H, Intros]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (ConstructorSeqTL[SS, H, Intros]) => Boolean): ConstructorSeqTL[SS, H, Intros]
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toEnsuring[ConstructorSeqTL[SS, H, Intros]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): ConstructorSeqTL[SS, H, Intros]
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toEnsuring[ConstructorSeqTL[SS, H, Intros]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): ConstructorSeqTL[SS, H, Intros]
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toEnsuring[ConstructorSeqTL[SS, H, Intros]] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toStringFormat[ConstructorSeqTL[SS, H, Intros]] 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 induc[C <: Term with Subs[C], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](Xs: Func[H, Typ[C]])(implicit mapper: ConstructorSeqMapper[SS, C, H, RecType, InducType, Intros]): InducType
returns the term
ind_W, Xfor inductively defining function to the type familyXson W from the inductive typeW = typ; an implicitmapperis used, which also allows calculation of the typeRecType.returns the term
ind_W, Xfor inductively defining function to the type familyXson W from the inductive typeW = typ; an implicitmapperis used, which also allows calculation of the typeRecType.- RecType
not used here, but part of the definition of the
mapper.- InducType
the type of the
inducfunction returned.
- def inducE[C <: Term with Subs[C]](Xs: Func[H, Typ[C]]): InducType forSome {type InducType <: Term with Subs[InducType]}
Existential typed version of induc to be used at runtime if necessary.
- val intros: Intros
The introduction rules.
- 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()
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def rec[C <: Term with Subs[C], RecType <: Term with Subs[RecType], InducType <: Term with Subs[InducType]](X: Typ[C])(implicit mapper: ConstructorSeqMapper[SS, C, H, RecType, InducType, Intros]): RecType
returns the term
rec_W, Xfor recursively defining function toXfrom the inductive typeW = typ; an implicitmapperis used, which also allows calculation of the typeRecType.returns the term
rec_W, Xfor recursively defining function toXfrom the inductive typeW = typ; an implicitmapperis used, which also allows calculation of the typeRecType.- RecType
type of the
recfunction returned;- InducType
not used here, but part of the definition of the
mapper.- X
the codomain to which we wish to define recursive functions - the only one we need to specify;
- def recE[C <: Term with Subs[C]](X: Typ[C]): RecType forSome {type RecType <: Term with Subs[RecType]}
Existential typed version of rec for use at runtime if neccesary.
- val seqDom: ConstructorSeqDom[SS, H, Intros]
- def subs(x: Term, y: Term): ConstructorSeqTL[SS, H, Intros]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- val typ: Typ[H]
- 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 |:[S <: HList, ConstructorType <: Term with Subs[ConstructorType]](head: ConstructorTL[S, H, ConstructorType]): ConstructorSeqTL[::[S, SS], H, ::[ConstructorType, Intros]]
Prepend to the sequence of introduction rules.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def →[B](y: B): (ConstructorSeqTL[SS, H, Intros], B)
- Implicit
- This member is added by an implicit conversion from ConstructorSeqTL[SS, H, Intros] toArrowAssoc[ConstructorSeqTL[SS, H, Intros]] 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.