OAI/NumberTheory/SingleFold/RationalCodes.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SingleFold.RationalCode line 7
  2. def OAI.SingleFold.RationalCode.Valid line 18
  3. def OAI.SingleFold.RationalCode.value line 22
  4. lemma OAI.SingleFold.RationalCode.den_pos line 24
  5. lemma OAI.SingleFold.RationalCode.inverse_lt line 28
  6. lemma OAI.SingleFold.RationalCode.inverse_mod line 32
  7. lemma OAI.SingleFold.RationalCode.reduced line 38
  8. lemma OAI.SingleFold.RationalCode.abs_num line 41
  9. lemma OAI.SingleFold.RationalCode.canonical line 47
  10. lemma OAI.SingleFold.RationalCode.positive_num line 58
  11. lemma OAI.SingleFold.RationalCode.negative_num line 64
  12. theorem OAI.SingleFold.RationalCode.unique line 70
  13. lemma OAI.SingleFold.RationalCode.inverse_exists line 95
  14. theorem OAI.SingleFold.RationalCode.existsUnique line 106
  15. theorem OAI.SingleFold.Compiler.SF.congr line 135
  16. theorem OAI.SingleFold.Compiler.SF.and line 138
  17. theorem OAI.SingleFold.Compiler.SF.or line 141
  18. theorem OAI.SingleFold.Compiler.SF.reindex line 144
  19. theorem OAI.SingleFold.Compiler.SF.all line 146
  20. theorem OAI.SingleFold.Compiler.SF.eq line 148
  21. theorem OAI.SingleFold.Compiler.SF.le line 149
  22. theorem OAI.SingleFold.Compiler.SF.lt line 150
  23. theorem OAI.SingleFold.Compiler.SF.ex line 151
  24. structure OAI.SingleFold.RationalCompiler.FractionPoly line 160
  25. def OAI.SingleFold.RationalCompiler.FractionPoly.value line 166
  26. def OAI.SingleFold.RationalCompiler.FractionPoly.const line 167
  27. def OAI.SingleFold.RationalCompiler.FractionPoly.add line 168
  28. def OAI.SingleFold.RationalCompiler.FractionPoly.mul line 169
  29. def OAI.SingleFold.RationalCompiler.FractionPoly.neg line 170
  30. lemma OAI.SingleFold.RationalCompiler.FractionPoly.const_value line 172
  31. lemma OAI.SingleFold.RationalCompiler.FractionPoly.add_value line 174
  32. lemma OAI.SingleFold.RationalCompiler.FractionPoly.mul_value line 180
  33. lemma OAI.SingleFold.RationalCompiler.FractionPoly.neg_value line 183
  34. lemma OAI.SingleFold.RationalCompiler.FractionPoly.eq_iff line 186
  35. lemma OAI.SingleFold.RationalCompiler.FractionPoly.le_iff line 194
  36. lemma OAI.SingleFold.RationalCompiler.FractionPoly.guarded_eq line 202
  37. lemma OAI.SingleFold.RationalCompiler.FractionPoly.guarded_le line 209
  38. def OAI.SingleFold.RationalCompiler.code line 218
  39. def OAI.SingleFold.RationalCompiler.tuple line 219
  40. lemma OAI.SingleFold.RationalCompiler.code_tuple line 220
  41. lemma OAI.SingleFold.RationalCompiler.tuple_code line 221
  42. def OAI.SingleFold.RationalCompiler.Valid line 223
  43. def OAI.SingleFold.RationalCompiler.value line 224
  44. def OAI.SingleFold.RationalCompiler.input line 226
  45. lemma OAI.SingleFold.RationalCompiler.input_value line 228
  46. lemma OAI.SingleFold.RationalCompiler.input_pos line 231
  47. lemma OAI.SingleFold.RationalCompiler.valid_single_fold line 237
  48. inductive OAI.SingleFold.RationalCompiler.Expr line 253
  49. def OAI.SingleFold.RationalCompiler.Expr.eval line 261
  50. def OAI.SingleFold.RationalCompiler.Expr.compile line 267
  51. lemma OAI.SingleFold.RationalCompiler.Expr.compile_spec line 273
  52. lemma OAI.SingleFold.RationalCompiler.Expr.eq_single_fold line 284
  53. lemma OAI.SingleFold.RationalCompiler.Expr.le_single_fold line 291
  54. def OAI.SingleFold.Compiler.Semi line 303
  55. theorem OAI.SingleFold.Compiler.Semi.congr line 306
  56. theorem OAI.SingleFold.Compiler.Semi.not line 308
  57. theorem OAI.SingleFold.Compiler.Semi.and line 310
  58. theorem OAI.SingleFold.Compiler.Semi.or line 314
  59. theorem OAI.SingleFold.Compiler.Semi.reindex line 316
  60. theorem OAI.SingleFold.Compiler.Semi.eq line 318
  61. theorem OAI.SingleFold.Compiler.Semi.le line 323
  62. theorem OAI.SingleFold.Compiler.Semi.lt line 325
  63. theorem OAI.SingleFold.Compiler.Semi.all line 327
  64. lemma OAI.SingleFold.RationalCompiler.valid_semi line 343
  65. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 360) line 360
  66. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 361) line 361
  67. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 362) line 362
  68. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 363) line 363
  69. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 364) line 364
  70. instance OAI.SingleFold.RationalCompiler.Expr.(instance at line 365) line 365
  71. lemma OAI.SingleFold.RationalCompiler.Expr.eval_add line 366
  72. lemma OAI.SingleFold.RationalCompiler.Expr.eval_mul line 367
  73. lemma OAI.SingleFold.RationalCompiler.Expr.eval_neg line 368
  74. lemma OAI.SingleFold.RationalCompiler.Expr.eval_sub line 369
  75. lemma OAI.SingleFold.RationalCompiler.Expr.eval_nat line 370
  76. lemma OAI.SingleFold.RationalCompiler.Expr.eval_ofNat line 371
  77. lemma OAI.SingleFold.RationalCompiler.Expr.eval_zero line 372
  78. lemma OAI.SingleFold.RationalCompiler.Expr.eval_one line 373
  79. lemma OAI.SingleFold.RationalCompiler.Expr.eval_var line 374
  80. lemma OAI.SingleFold.RationalCompiler.Expr.eval_pow line 375
  81. lemma OAI.SingleFold.RationalCompiler.Expr.eq_under line 380
  82. lemma OAI.SingleFold.RationalCompiler.Expr.le_under line 391
  83. def OAI.SingleFold.RationalCode.encode line 406
  84. lemma OAI.SingleFold.RationalCode.encode_valid line 407
  85. lemma OAI.SingleFold.RationalCode.encode_value line 408
  86. lemma OAI.SingleFold.RationalCode.eq_encode line 409