OAI/Combinatorics/ThinTrees/Arithmetic/BinaryArithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Binary arithmetic.

  1. def OAI.CurrentKS.Realization.wordCons line 17
  2. instance OAI.CurrentKS.Realization.poly_wordCons line 26
  3. def OAI.CurrentKS.Realization.binaryToRat line 28
  4. instance OAI.CurrentKS.Realization.poly_binaryToRat line 35
  5. lemma OAI.CurrentKS.Realization.intPayload_natCast line 37
  6. def OAI.CurrentKS.Realization.binaryDiv line 39
  7. instance OAI.CurrentKS.Realization.poly_binaryDiv line 44
  8. def OAI.CurrentKS.Realization.binaryMod line 46
  9. instance OAI.CurrentKS.Realization.poly_binaryMod line 55
  10. def OAI.CurrentKS.Realization.binaryModUnary line 57
  11. instance OAI.CurrentKS.Realization.poly_binaryModUnary line 59
  12. def OAI.CurrentKS.Realization.ratDenRat line 71
  13. instance OAI.CurrentKS.Realization.poly_ratDenRat line 72
  14. def OAI.CurrentKS.Realization.scalarProductBinary line 74
  15. instance OAI.CurrentKS.Realization.poly_scalarProductBinary line 84