OAI/Computability/DeterministicSum/Expressions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite arithmetic expressions and their costed compilation.

  1. inductive OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic line 11
  2. def OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic.op line 15
  3. def OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic.value line 18
  4. def OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic.Valid line 21
  5. lemma OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic.value_lt line 27
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.Arithmetic.run line 36
  7. inductive OAI.DeterministicThreeSum.Structured.Indexed.Expr line 43
  8. def OAI.DeterministicThreeSum.Structured.Indexed.Expr.value line 48
  9. def OAI.DeterministicThreeSum.Structured.Indexed.Expr.Valid line 53
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.Expr.value_lt line 58
  11. def OAI.DeterministicThreeSum.Structured.Indexed.Expr.compile line 65
  12. def OAI.DeterministicThreeSum.Structured.Indexed.Expr.cost line 71
  13. theorem OAI.DeterministicThreeSum.Structured.Indexed.Expr.compile_correct line 76
  14. inductive OAI.DeterministicThreeSum.Structured.Indexed.RingOp line 113
  15. def OAI.DeterministicThreeSum.Structured.Indexed.RingOp.bin line 116
  16. def OAI.DeterministicThreeSum.Structured.Indexed.RingOp.raw line 118
  17. def OAI.DeterministicThreeSum.Structured.Indexed.RingOp.command line 120
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.RingOp.run line 124
  19. inductive OAI.DeterministicThreeSum.Structured.Indexed.Scalar line 140
  20. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.value line 146
  21. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.Valid line 152
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.value_lt line 159
  23. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.compile line 172
  24. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.cost line 179
  25. theorem OAI.DeterministicThreeSum.Structured.Indexed.Scalar.compile_correct line 185