object HoTTPost
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- HoTTPost
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- case class Apex[P](base: P) extends Product with Serializable
- case class HoTTPostData(number: Int, posts: Vector[(PostData[_, HoTTPost, ID], ID, Set[ID])]) extends Product with Serializable
- type ID = (Int, Int)
- case class IsleNormalizedEquationNodes(eqn: Set[EquationNode]) extends Product with Serializable
- case class TunedLocalProver(lp: LocalProver) extends 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 allPostFullData(web: HoTTPost): Vector[(PostData[_, HoTTPost, ID], ID, Set[ID])]
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- lazy val b1: BiPostable[Lemmas, HoTTPost, ID]
- lazy val b2: BiPostable[ChompResult, HoTTPost, ID]
- 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
- lazy val eqnUpdate: PostResponse[HoTTPost, ID]
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- implicit def equationNodeQuery: Queryable[Set[EquationNode], HoTTPost]
- implicit def equationQuery: Queryable[Set[Equation], HoTTPost]
- lazy val expEvToEqns: PostResponse[HoTTPost, ID]
- def fansiLog(post: PostData[_, HoTTPost, ID]): Future[Unit]
- def findInWeb(web: HoTTPost, index: ID): Option[(PostData[_, HoTTPost, ID], Set[ID])]
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- implicit def hottPostDataQuery: Queryable[HoTTPostData, HoTTPost]
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- lazy val isleNormalizeEqns: PostResponse[HoTTPost, ID]
- lazy val lemmaToTangentProver: PostResponse[HoTTPost, ID]
- lazy val lpFromInit: PostResponse[HoTTPost, ID]
- lazy val lpFromTG: PostResponse[HoTTPost, ID]
- lazy val lpLemmas: PostResponse[HoTTPost, ID]
- implicit def lpStepQuery: LocalQueryable[LocalProverStep, HoTTPost, ID]
- lazy val lpToChomp: PostResponse[HoTTPost, ID]
- lazy val lpToExpEv: PostResponse[HoTTPost, ID]
- lazy val lpToTermResult: PostResponse[HoTTPost, ID]
- lazy val lptLemmas: PostResponse[HoTTPost, ID]
- lazy val lptToExpEv: PostResponse[HoTTPost, ID]
- lazy val lptToTermResult: PostResponse[HoTTPost, ID]
- def mutWebBuffers(web: HoTTPost): Vector[ErasableWebBuffer[_, ID]]
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- lazy val normEqnUpdate: PostResponse[HoTTPost, ID]
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- implicit val postChomp: Postable[ChompResult, HoTTPost, ID]
- implicit val postEqnNodes: Postable[Set[EquationNode], HoTTPost, ID]
- implicit val postError: Postable[Throwable, HoTTPost, ID]
- implicit val postExpEv: Postable[ExpressionEquationSolver, HoTTPost, ID]
- implicit val postFinal: Postable[FinalState, HoTTPost, ID]
- implicit val postGenEqns: Postable[GeneratedEquationNodes, HoTTPost, ID]
- implicit val postHNil: Postable[HNil, HoTTPost, ID]
- implicit def postHistory: PostHistory[HoTTPost, ID]
- implicit val postInit: Postable[InitState, HoTTPost, ID]
- implicit val postIslNrmEqns: Postable[IsleNormalizedEquationNodes, HoTTPost, ID]
- implicit val postLP: Postable[LocalProver, HoTTPost, ID]
- implicit val postLPT: Postable[LocalTangentProver, HoTTPost, ID]
- implicit val postLemmas: Postable[Lemmas, HoTTPost, ID]
- implicit val postResult: Postable[TermResult, HoTTPost, ID]
- implicit val postTg: Postable[TermGenParams, HoTTPost, ID]
- implicit def postToLeaves[P](implicit arg0: scala.reflect.api.JavaUniverse.TypeTag[P], bp: Postable[P, HoTTPost, ID], dg: DataGetter[P, HoTTPost, ID]): Postable[Apex[P], HoTTPost, ID]
- implicit val postTunedLP: Postable[TunedLocalProver, HoTTPost, ID]
- implicit val postUnit: Postable[Unit, HoTTPost, ID]
- lazy val recomputeFromInit: PostResponse[HoTTPost, ID]
- implicit val repPost: Postable[Map[Variable[_], Vector[Double]], HoTTPost, ID]
- def skipDeleted(web: HoTTPost, id: ID): Set[ID]
- def skipDeletedStep(web: HoTTPost, id: ID): Option[Set[ID]]
- implicit val someInitQuery: LatestAnswer[Some[InitState], HoTTPost, ID]
- implicit val someTGQuery: LatestAnswer[Some[TermGenParams], HoTTPost, ID]
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- lazy val termResultToChomp: PostResponse[HoTTPost, ID]
- lazy val termResultToEquations: PostResponse[HoTTPost, ID]
- implicit def termSetQuery: Queryable[Set[Term], HoTTPost]
- def testGet: PostHistory[HoTTPost, ID]
- def toString(): String
- Definition Classes
- AnyRef → Any
- lazy val tuneLP: PostResponse[HoTTPost, ID]
- 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