Packages

object PolymathProof

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

Value Members

  1. val b: Func[RepTerm[SafeLong], RepTerm[Word]]
  2. val bIsc: Equality[RepTerm[Rational]]
  3. val baseCase: PosWit
  4. val bnd: RepTerm[Rational]
  5. val c: Func[RepTerm[SafeLong], RepTerm[Word]]
  6. val c1: Equality[RepTerm[Word]]
  7. val c2: Equality[RepTerm[Word]]
  8. val cbnd: Func[PosWit, PosWit]
  9. val conjInv: FuncLike[RepTerm[Word], FuncLike[RepTerm[Word], Equality[RepTerm[Rational]]]]
  10. val d: Func[RepTerm[SafeLong], RepTerm[Word]]
  11. val dIsc: Equality[RepTerm[Word]]
  12. val exprBound: PosWitSum
  13. val f: Func[RepTerm[SafeLong], RepTerm[Rational]]
  14. val g: RepTerm[Word]
  15. val grpe: RepTerm[Word]
  16. val h: RepTerm[Word]
  17. val hyp: PosWit
  18. val l: Func[RepTerm[Word], RepTerm[Rational]]
  19. val lbIsld: Equality[RepTerm[Rational]]
  20. val lbnBounded: PosWitSum
  21. val lbnBoundedlcnlylz: PosWitSum
  22. val lemma: Func[RepTerm[SafeLong], Pos]
  23. val lemmaProof: Induc[PosWit]
  24. val n: RepTerm[SafeLong]
  25. val pown: Func[RepTerm[Word], RepTerm[Word]]
  26. val r: Func[scalahott.NatRing.LocalTerm, scalahott.QField.LocalTerm]
  27. val s: RepTerm[Word]
  28. val step: PosWit
  29. val t: RepTerm[Word]
  30. val t1: RepTerm[Word]
  31. val t2: RepTerm[Word]
  32. val thmBound: RepTerm[Rational]
  33. val thmProof: PosWit
  34. val triang: FuncLike[RepTerm[Word], FuncLike[RepTerm[Word], PosWit]]
  35. val w: RepTerm[Word]
  36. val wy: RepTerm[Word]
  37. val wyn: RepTerm[Word]
  38. val x: RepTerm[Word]
  39. val x2n: RepTerm[Word]
  40. val x2nExpr: Equality[RepTerm[Word]]
  41. val xnConjwyn: Equality[RepTerm[Word]]
  42. val xnConjzwbarn: Equality[RepTerm[Word]]
  43. val xnxnExpr: Equality[RepTerm[Word]]
  44. val y: RepTerm[Word]
  45. val z: RepTerm[Word]
  46. val zwbar: RepTerm[Word]
  47. val zwbarn: RepTerm[Word]