object IdentityTyp extends Serializable
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- IdentityTyp
- Serializable
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- case class InducFn[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], targetFmly: FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]], data: FuncLike[U, V], start: U, end: U) extends IndInducFuncLike[Equality[U], V, Func[U, Func[U, Typ[Term]]], FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]]] with Product with Serializable
inductive definition for identity type family.
- case class RecFn[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], target: Typ[V], data: Func[U, V], start: U, end: U) extends IndRecFunc[Term, V, Func[U, Func[U, Typ[Term]]]] with Product with Serializable
recursive definition on identity type families
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
- lazy val A: Typ[Term]
- lazy val B: Typ[Term]
- def apf[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]
- lazy val apfTerm: FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Func[Term, Term], FuncLike[Term, FuncLike[Term, Func[Equality[Term], Equality[Term]]]]]]]
- 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()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- lazy val f: Func[Term, Term]
- def get[U <: Term with Subs[U]](lhs: U, rhs: U): IdentityTyp[U]
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- lazy val idFunc: FuncLike[Typ[Term], Func[Term, Func[Term, IdentityTyp[Term]]]]
- def induc[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], targetFmly: FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]]): Func[FuncLike[U, V], FuncLike[U, FuncLike[U, Func[Equality[U], V]]]]
inductive definition for identity type family.
- def induced[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]
equality induced by a (pure) function term with type
x =y -> f(x) = f(y)as function ofxandy - def inducedWit[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]
- 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 preTrans[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]
- def rec[U <: Term with Subs[U], V <: Term with Subs[V]](dom: Typ[U], target: Typ[V]): Func[Func[U, V], FuncLike[U, FuncLike[U, Func[Equality[U], V]]]]
recursive definition for identity type family
- lazy val reflTerm: FuncLike[Typ[Term], FuncLike[Term, Refl[Term]]]
- def symm[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[U]]]]
symmetry term of type
x = y -> y = xas a function ofxandy - lazy val symmTerm: FuncLike[Typ[Term], FuncLike[Term, FuncLike[Term, Func[Equality[Term], Equality[Term]]]]]
- def symmWit[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[U]]]]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- def trans[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]
transitivity term of type
x = y -> y = z -> x = zas a function ofx,yandz - lazy val transTerm: FuncLike[Typ[Term], FuncLike[Term, FuncLike[Term, FuncLike[Term, Func[Equality[Term], Func[Equality[Term], Equality[Term]]]]]]]
- def transWit[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]
- def transport[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, Typ[V]]): FuncLike[U, FuncLike[U, Func[Equality[U], Func[V, V]]]]
transport: term with type
x = y -> f(x) -> f(y)as function ofxandy - def transportWit[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, Typ[V]]): FuncLike[U, FuncLike[U, Func[Equality[U], Func[V, V]]]]
- 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])
- lazy val x: Term
- lazy val y: Term
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated