Packages

object HoTTPostWeb

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. HoTTPostWeb
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type ID = (Int, Int)

Value Members

  1. implicit val b1: BiPostable[HNil, HoTTPostWeb, ID]
  2. implicit val b10: BiPostable[GeneratedEquationNodes, HoTTPostWeb, ID]
  3. implicit val b11: BiPostable[TermResult, HoTTPostWeb, ID]
  4. implicit val b12: BiPostable[FinalState, HoTTPostWeb, ID]
  5. implicit val b13: BiPostable[InitState, HoTTPostWeb, ID]
  6. implicit val b14: BiPostable[SeekInstances, HoTTPostWeb, ID]
  7. implicit val b15: BiPostable[Instance, HoTTPostWeb, ID]
  8. implicit val b16: BiPostable[SeekGoal, HoTTPostWeb, ID]
  9. implicit val b17: BiPostable[Lemmas, HoTTPostWeb, ID]
  10. implicit val b18: BiPostable[UseLemmaDistribution, HoTTPostWeb, ID]
  11. implicit val b19: BiPostable[UseLemma, HoTTPostWeb, ID]
  12. implicit val b2: BiPostable[Unit, HoTTPostWeb, ID]
  13. implicit val b20: BiPostable[Consequence, HoTTPostWeb, ID]
  14. implicit val b21: BiPostable[FromAll, HoTTPostWeb, ID]
  15. implicit val b22: BiPostable[FunctionForGoal, HoTTPostWeb, ID]
  16. implicit val b23: BiPostable[Cap.type, HoTTPostWeb, ID]
  17. implicit val b24: BiPostable[ConsiderInductiveTypes, HoTTPostWeb, ID]
  18. implicit val b25: BiPostable[TautologyInitState, HoTTPostWeb, ID]
  19. implicit val b26: BiPostable[TangentBaseCompleted.type, HoTTPostWeb, ID]
  20. implicit val b27: BiPostable[EquationsCompleted.type, HoTTPostWeb, ID]
  21. implicit val b28: BiPostable[BaseMixinLemmas, HoTTPostWeb, ID]
  22. implicit val b29: BiPostable[TangentLemmas, HoTTPostWeb, ID]
  23. implicit val b3: BiPostable[Weight, HoTTPostWeb, ID]
  24. implicit val b30: BiPostable[SpecialInitState, HoTTPostWeb, ID]
  25. implicit val b31: BiPostable[TangentBaseState, HoTTPostWeb, ID]
  26. implicit val b32: BiPostable[UsedLemmas, HoTTPostWeb, ID]
  27. implicit val b33: BiPostable[FromAny, HoTTPostWeb, ID]
  28. implicit val b34: BiPostable[NarrowOptimizeGenerators, HoTTPostWeb, ID]
  29. implicit val b35: BiPostable[OptimalInitial, HoTTPostWeb, ID]
  30. implicit val b36: BiPostable[ExstInducDefn, HoTTPostWeb, ID]
  31. implicit val b37: BiPostable[Contradicts, HoTTPostWeb, ID]
  32. implicit val b38: BiPostable[ProofLambda, HoTTPostWeb, ID]
  33. implicit val b39: BiPostable[FailedToProve, HoTTPostWeb, ID]
  34. implicit val b4: BiPostable[LocalProver, HoTTPostWeb, ID]
  35. implicit val b40: BiPostable[RepresentationMap, HoTTPostWeb, ID]
  36. implicit val b5: BiPostable[ChompResult, HoTTPostWeb, ID]
  37. implicit val b6: BiPostable[ExpressionEquationSolver, HoTTPostWeb, ID]
  38. implicit val b7: BiPostable[LocalTangentProver, HoTTPostWeb, ID]
  39. implicit val b8: BiPostable[Contradicted, HoTTPostWeb, ID]
  40. implicit val b9: BiPostable[Proved, HoTTPostWeb, ID]
  41. implicit def equationNodeQuery: Queryable[Set[EquationNode], HoTTPostWeb]
  42. implicit def equationQuery: Queryable[Set[Equation], HoTTPostWeb]
  43. implicit val history: PostHistory[HoTTPostWeb, ID]
  44. val polyImpl: ::[BiPostable[FunctionForGoal, HoTTPostWeb, ID], ::[BiPostable[FromAll, HoTTPostWeb, ID], ::[BiPostable[Consequence, HoTTPostWeb, ID], ::[BiPostable[UseLemma, HoTTPostWeb, ID], ::[BiPostable[UseLemmaDistribution, HoTTPostWeb, ID], ::[BiPostable[Lemmas, HoTTPostWeb, ID], ::[BiPostable[SeekGoal, HoTTPostWeb, ID], ::[BiPostable[Instance, HoTTPostWeb, ID], ::[BiPostable[SeekInstances, HoTTPostWeb, ID], ::[BiPostable[InitState, HoTTPostWeb, ID], ::[BiPostable[FinalState, HoTTPostWeb, ID], ::[BiPostable[TermResult, HoTTPostWeb, ID], ::[BiPostable[GeneratedEquationNodes, HoTTPostWeb, ID], ::[BiPostable[Proved, HoTTPostWeb, ID], ::[BiPostable[Contradicted, HoTTPostWeb, ID], ::[BiPostable[LocalTangentProver, HoTTPostWeb, ID], ::[BiPostable[ExpressionEquationSolver, HoTTPostWeb, ID], ::[BiPostable[ChompResult, HoTTPostWeb, ID], ::[BiPostable[LocalProver, HoTTPostWeb, ID], ::[BiPostable[Weight, HoTTPostWeb, ID], ::[BiPostable[Unit, HoTTPostWeb, ID], ::[BiPostable[HNil, HoTTPostWeb, ID], HNil]]]]]]]]]]]]]]]]]]]]]]
  45. val polyImpl2: ::[BiPostable[RepresentationMap, HoTTPostWeb, ID], ::[BiPostable[FailedToProve, HoTTPostWeb, ID], ::[BiPostable[ProofLambda, HoTTPostWeb, ID], ::[BiPostable[Contradicts, HoTTPostWeb, ID], ::[BiPostable[ExstInducDefn, HoTTPostWeb, ID], ::[BiPostable[OptimalInitial, HoTTPostWeb, ID], ::[BiPostable[NarrowOptimizeGenerators, HoTTPostWeb, ID], ::[BiPostable[FromAny, HoTTPostWeb, ID], ::[BiPostable[UsedLemmas, HoTTPostWeb, ID], ::[BiPostable[TangentBaseState, HoTTPostWeb, ID], ::[BiPostable[SpecialInitState, HoTTPostWeb, ID], ::[BiPostable[TangentLemmas, HoTTPostWeb, ID], ::[BiPostable[BaseMixinLemmas, HoTTPostWeb, ID], ::[BiPostable[EquationsCompleted.type, HoTTPostWeb, ID], ::[BiPostable[TangentBaseCompleted.type, HoTTPostWeb, ID], ::[BiPostable[TautologyInitState, HoTTPostWeb, ID], ::[BiPostable[ConsiderInductiveTypes, HoTTPostWeb, ID], ::[BiPostable[Cap.type, HoTTPostWeb, ID], HNil]]]]]]]]]]]]]]]]]]
  46. implicit def termSetQuery: Queryable[Set[Term], HoTTPostWeb]
  47. val tw: Postable[WithWeight[Proved], HoTTPostWeb, ID]