object Unify
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- Unify
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- case class UnifyApplnException(func: Term, arg: Term, freeVars: Vector[Term], error: Throwable) extends Exception with Product with Serializable
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 appln(func: Term, arg: Term, freeVars: Vector[Term] = Vector()): Option[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()
- def dependsOn(term: Term): (Vector[Term]) => Boolean
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def extraVars(v: Vector[Term], m: Map[Term, Term]): Vector[Term]
- 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
- def mergeAll[U, V](xs: Option[Map[U, V]]*): Option[Map[U, V]]
- def mergeMaps[U, V](x: Map[U, V], y: Map[U, V]): Option[Map[U, V]]
- def mergeOptMaps[U, V](x: Option[Map[U, V]], y: Option[Map[U, V]]): Option[Map[U, V]]
- def multisub[U <: Term with Subs[U]](x: U, m: Map[Term, Term]): U
- 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 purgeInv(r1: Term, inv1: Set[(Term, Term)], r2: Term, inv2: Set[(Term, Term)], freeVars: (Term) => Boolean): Set[(Term, Term)]
- def purgeVector(r2: Term, inv2: Set[(Term, Term)], invVector: Vector[(Term, Set[(Term, Term)])], freeVars: (Term) => Boolean): (Term, Set[(Term, Term)])
- def purgedInvVector(invVector: Vector[(Term, Set[(Term, Term)])], accum: Vector[(Term, Set[(Term, Term)])] = Vector(), freeVars: (Term) => Boolean = HoTT.isVar): Vector[(Term, Set[(Term, Term)])]
- Annotations
- @tailrec()
- def purgedPairs(fxs: Set[(Term, Term)]): Set[(Term, Term)]
- def purgedPairsList(fxs: List[(Term, Term)], accum: List[(Term, Term)] = List()): List[(Term, Term)]
- Annotations
- @tailrec()
- def subsApply(func: Term, arg: Term, unifMap: Map[Term, Term], freeVars: Vector[Term]): Option[Term]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def targetCodomain(func: Term, codomain: Term, freeVars: Vector[Term] = Vector()): Option[Term]
Given a function and a target type, optionally returns a function with eventual codomain the given type; this is done by attempting to unify, filling in parameters where they are determined and returing lambdas if all parameters work.
- def targetCodomainStrict(func: Term, codomain: Term, freeVars: Vector[Term] = Vector()): Option[Term]
Given a function and a target type, optionally returns a function with eventual codomain the given type; this is done by attempting to unify, filling in parameters where they are determined and returing lambdas if all parameters work.
- def toString(): String
- Definition Classes
- AnyRef → Any
- def unifApply(func: Term, arg: Term, freeVars: Vector[Term]): Option[Term]
- def unify(lhs: Term, rhs: Term, freevars: (Term) => Boolean): Option[Map[Term, Term]]
- def unifyAll(freeVars: (Term) => Boolean)(xys: (Term, Term)*): Option[Map[Term, Term]]
- def unifyVector(xys: Vector[(Term, Term)], freeVars: (Term) => Boolean): Option[Map[Term, Term]]
- 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