OAI/Computability/QuantumFactoring/IntegerExpressions.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.IntExpr line 13

    Source documentation

    Balanced integers avoid a word-size-dependent signed representation.

    structure IntExpr (v : Type*) where
…
  2. def OAI.ExactQuantumFactoring.IntExpr.eval line 20
  3. def OAI.ExactQuantumFactoring.IntExpr.ofNat line 22
  4. def OAI.ExactQuantumFactoring.IntExpr.ofInt line 23
  5. def OAI.ExactQuantumFactoring.IntExpr.add line 24
  6. def OAI.ExactQuantumFactoring.IntExpr.negation line 25
  7. def OAI.ExactQuantumFactoring.IntExpr.sub line 26
  8. def OAI.ExactQuantumFactoring.IntExpr.mul line 27
  9. def OAI.ExactQuantumFactoring.IntExpr.scale line 30
  10. def OAI.ExactQuantumFactoring.IntExpr.toNat line 31
  11. def OAI.ExactQuantumFactoring.IntExpr.natAbs line 32
  12. def OAI.ExactQuantumFactoring.IntExpr.iteLe line 33
  13. lemma OAI.ExactQuantumFactoring.IntExpr.eval_ofNat line 36
  14. lemma OAI.ExactQuantumFactoring.IntExpr.eval_ofInt line 38
  15. lemma OAI.ExactQuantumFactoring.IntExpr.eval_add line 40
  16. lemma OAI.ExactQuantumFactoring.IntExpr.eval_negation line 43
  17. lemma OAI.ExactQuantumFactoring.IntExpr.eval_sub line 45
  18. lemma OAI.ExactQuantumFactoring.IntExpr.eval_mul line 47
  19. lemma OAI.ExactQuantumFactoring.IntExpr.eval_scale line 50
  20. lemma OAI.ExactQuantumFactoring.IntExpr.eval_toNat line 52
  21. lemma OAI.ExactQuantumFactoring.IntExpr.eval_natAbs line 54
  22. lemma OAI.ExactQuantumFactoring.IntExpr.eval_iteLe line 57