OAI/Computability/MatchingCount/IntegerRoutine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.StackCode.intParts line 10
  2. def OAI.BinaryMatching.StackCode.fromParts line 11
  3. instance OAI.BinaryMatching.StackCode.(instance at line 12) line 12
  4. lemma OAI.BinaryMatching.StackCode.encode_int line 13
  5. lemma OAI.BinaryMatching.StackCode.fromParts_parts line 14
  6. lemma OAI.BinaryMatching.StackCode.intParts_nat line 20
  7. lemma OAI.BinaryMatching.StackCode.intParts_fromParts line 23
  8. theorem OAI.BinaryMatching.StackCode.Poly.intParts_poly line 34
  9. theorem OAI.BinaryMatching.StackCode.Poly.natCastInt line 38
  10. theorem OAI.BinaryMatching.StackCode.Poly.natToInt line 45
  11. theorem OAI.BinaryMatching.StackCode.Poly.fromParts_poly line 47
  12. theorem OAI.BinaryMatching.StackCode.Poly.intNatAbs line 56
  13. theorem OAI.BinaryMatching.StackCode.Poly.intSign line 60
  14. theorem OAI.BinaryMatching.StackCode.Poly.intNeg line 64
  15. def OAI.BinaryMatching.StackCode.Poly.addParts line 68
  16. lemma OAI.BinaryMatching.StackCode.Poly.addParts_eq line 78
  17. theorem OAI.BinaryMatching.StackCode.Poly.intAdd line 87
  18. theorem OAI.BinaryMatching.StackCode.Poly.intSub line 92
  19. theorem OAI.BinaryMatching.StackCode.Poly.intMul line 96
  20. theorem OAI.BinaryMatching.StackCode.Poly.intLE line 109
  21. theorem OAI.BinaryMatching.StackCode.Poly.intLT line 114
  22. theorem OAI.BinaryMatching.StackCode.Poly.intEQ line 118
  23. theorem OAI.BinaryMatching.StackCode.Poly.intMin line 123
  24. theorem OAI.BinaryMatching.StackCode.Poly.intMax line 126
  25. theorem OAI.BinaryMatching.StackCode.Poly.intToNat line 129
  26. theorem OAI.BinaryMatching.StackCode.Poly.intLt_apply line 133
  27. theorem OAI.BinaryMatching.StackCode.Poly.intLe_apply line 135