object TermPatterns
Patterns, in the sense of Translator.Pattern, as well as some builders for various kinds of HoTT terms. Includes matching recursively and inductively defined functions.
- Alphabetic
- By Inheritance
- TermPatterns
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
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
- val absPair: Pattern[Term, II]
matches all pairs
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def buildIndDef(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, Term, _]] = (_) => None): (Term, (Term, Vector[Term])) => Option[Term]
returns inductively defined function as function of domain, codomain and definition data
returns inductively defined function as function of domain, codomain and definition data
- inds
inductive types defined (other than products etc)
- def buildIndIndDef(inds: (Term) => Option[IndexedConstructorSeqDom[_, Term, _, _, _]] = (_) =>
None): (Vector[Term], (Term, (Term, Vector[Term]))) => Option[Term]
returns indexed inductively defined function as function of domain, codomain and definition data
returns indexed inductively defined function as function of domain, codomain and definition data
- inds
inductive types defined (other than equality)
- def buildIndRecDef(inds: (Term) => Option[IndexedConstructorSeqDom[_, Term, _, _, _]] = (_) =>
None): (Vector[Term], (Term, (Term, Vector[Term]))) => Option[Term]
returns indexed recursively defined function as function of domain, codomain and definition data
returns indexed recursively defined function as function of domain, codomain and definition data
- inds
indexed inductive types defined (other than equality)
- def buildRecDef(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, _, _]] = (_) =>
None): (Term, (Term, Vector[Term])) => Option[Term]
returns recursively defined function as function of domain, codomain and definition data
returns recursively defined function as function of domain, codomain and definition data
- inds
inductive types defined (other that products etc)
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- val depPairTerm: Pattern[Term, III]
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- val equation: Pattern[Term, II]
matches identity (equality) type, returns lhs and rhs
- val firstIncl: Pattern[Term, II]
matches
i_1(a), the first inclusion function, returns the type and value - def fm[U <: Term with Subs[U]](dom: Typ[U], fmly: Term): Func[U, Typ[_]] forSome {type _ <: Term with Subs[_]}
- val foldedTerm: Pattern[Term, IV]
- val formalAppln: Pattern[Term, II]
matches formal applications
- val funcTyp: Pattern[Term, II]
matches function types, returning domain and codomain
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def getName(sym: AnySym): Option[Name]
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- val hashSymbolic: Pattern[Term, Named]
- val identityTyp: Pattern[Term, III]
matches identity (equality) type, returns domain, lhs and rhs
- val indInducFunc: Pattern[Term, IVIIV]
matches indexed inductively defined function, returns index, domain, codomain and definition data
- val indRecFunc: Pattern[Term, IVIIV]
matches idexed recursively defined function, returns index, domain, codomain and definition data
- val inducFunc: Pattern[Term, IIV]
matches inductively defined function, returns domain, codomain and definition data
- def inducFuncApplied(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, Term, _]]): Pattern[Term, Id]
- val introIndInducFunc: Pattern[Term, VIVIIV]
- val introIndRecFunc: Pattern[Term, VIVIIV]
- val introInducFunc: Pattern[Term, VIIV]
- val introRecFunc: Pattern[Term, VIIV]
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val lambdaAppln: Pattern[Term, II]
matches lambda definitions
- val lambdaFixedTriple: Pattern[Term, III]
- val lambdaTriple: Pattern[Term, III]
matches lambda applications and returns HoTT-type of the variable as well
- val mereWitness: Pattern[Term, II]
- val miscAppln: Pattern[Term, II]
- val natAddMorph: Pattern[Term, II]
- val natLiteral: Pattern[Term, N]
- val natProd: Pattern[Term, Un]
- val natSucc: Pattern[Term, Un]
- val natSum: Pattern[Term, Un]
- val natTyp: Pattern[Term, Un]
- val natUniv: Pattern[Term, Un]
- val natZero: Pattern[Term, Un]
- 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 numberedSymbolic(prefix: String): Pattern[Term, Numbered]
- val pairTerm: Pattern[Term, II]
- val piLam: Pattern[Term, II]
matches Pi-Type and returns the fibre as a lambda
- val piTriple: Pattern[Term, III]
matches Pi-Types, returns in the pi-lambda form with the HoTT-type of variable included.
- val piTyp: Pattern[Term, Id]
matches Pi-Type and returns the fibre
- val plusTyp: Pattern[Term, II]
matches coproduct type
- val prodTyp: Pattern[Term, II]
matches product types
- val prop: Pattern[Term, Un]
matches
Prop, the false type, returns() : Unitif matched - val propUniv: Pattern[Term, Un]
- val recFunc: Pattern[Term, IIV]
matches recursively defined function, returns domain, codomain and definition data
- def recFuncApplied(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, _, _]]): Pattern[Term, Id]
- val refl: Pattern[Term, II]
- val secondIncl: Pattern[Term, II]
matches
i_2(a), the second inclusion function, returns the type and value - val sigmaLam: Pattern[Term, II]
matches Sigma-Type and returns fibre as lambda
- val sigmaTriple: Pattern[Term, III]
matches Sigma-Types, returns in the pi-lambda form with the HoTT-type of variable included.
- val sigmaTyp: Pattern[Term, Id]
matches Sigma-Type and returns the fibre
- val star: Pattern[Term, Un]
matches
Star, the only element of the true typeUnit, returns() : Unitif matched - val stringRep: Pattern[Term, S]
- val symName: Pattern[Term, S]
matches a symbolic name, perhaps wrapped in
InnerSym, returns the name as aString - val symString: Pattern[Term, S]
- val symbolic: Pattern[Term, Named]
matches a symbolic name, perhaps wrapped in
InnerSym, returnsName - final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def termToExpr[E](univ: (Int) => Option[E])(implicit arg0: ExprLang[E]): OrElse[Term, E]
- def termToExprRaw[E](implicit arg0: ExprLang[E]): OrElse[Term, E]
- def toString(): String
- Definition Classes
- AnyRef → Any
- val unit: Pattern[Term, Un]
matches the true type
Unit, returns() : Unitif matched - val universe: Pattern[Term, N]
matches
Universe(n), returns the leveln - 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])
- val zero: Pattern[Term, Un]
matches
Zero, the false type, returns() : Unitif matched
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated