1. Top
  2. 6.5610-project
  3. Commits
6.5610-project

Cryptography final project

Commits at f1c8b8e7da9d0cde6e7991916c7a087e57e203e0

  1. f1c8b8e7 Update to Lean v4.31.0-rc1 Anthony Wang authored at Anthony Wang comitted at
  2. 6f73f4e5 Use toTypeExpr instead of manually constructing the exprs Anthony Wang authored at Anthony Wang comitted at
  3. 3d960056 Fix typo Well technically this is not a typo but I prefer ↦ since => is already used in match Anthony Wang authored at Anthony Wang comitted at
  4. fd2b9342 Crazy fun metaprogramming to autogenerate list of defs Anthony Wang authored at Anthony Wang comitted at
  5. b7c7b7ac Add unit_rec, support equality of types Anthony Wang authored at Anthony Wang comitted at
  6. b6f3134f Only 1500 (non-blank) lines now! Anthony Wang authored at Anthony Wang comitted at
  7. 3d419899 More tactics Anthony Wang authored at Anthony Wang comitted at
  8. 69078955 Merge pull request #1 from i-love-lean/add-macrolean Reorganize into microlean/ + macrolean/ i-love-lean authored at GitHub comitted at
  9. 6b8c2961 Use array instead of list Anthony Wang authored at Anthony Wang comitted at
  10. 64da70e0 Fix typos Anthony Wang authored at Anthony Wang comitted at
  11. 8ecccea8 Use OfNat typeclass for less jankiness Anthony Wang authored at Anthony Wang comitted at
  12. 8e8358a5 New clc tactic and better notation for type of Anthony Wang authored at Anthony Wang comitted at
  13. 36d802f5 Don't allow earlier defs to depend on later ones Anthony Wang authored at Anthony Wang comitted at
  14. 4557d4e2 Make theorems opaque (another 25x speedup!) Now it's like 5000x faster than the original or something? Anthony Wang authored at Anthony Wang comitted at
  15. 88731c6c add_comm ZKP example Anthony Wang authored at Anthony Wang comitted at
  16. 5f4c48ff Commit more slop Dan Klishch authored at Dan Klishch comitted at
  17. f720cd1a Update dbtypes Anthony Wang authored at Anthony Wang comitted at
  18. aa5a45f0 Better formatting for test output Anthony Wang authored at Anthony Wang comitted at
  19. 61d48690 Delete unused slop lemmas Anthony Wang authored at Anthony Wang comitted at
  20. 3b1e66a0 Technically not an elaborator Anthony Wang authored at Anthony Wang comitted at
  21. 2ef76866 More comments, rearrange some stuff Anthony Wang authored at Anthony Wang comitted at
  22. ddce1e73 SQRT 2 IS IRRATIONAL I also made the elaborator 5x faster yay Anthony Wang authored at Anthony Wang comitted at
  23. 052a7f67 Make the type checker 50x faster, some progress towards √2 irrational Anthony Wang authored at Anthony Wang comitted at
  24. 142d8bf6 INFINITE UNIVERSES (necessary for succ_ne_zero) Anthony Wang authored at Anthony Wang comitted at
  25. 467ad16e Move apb apr const to a more logical place Anthony Wang authored at Anthony Wang comitted at
  26. 05f5f38f Fix typos Anthony Wang authored at Anthony Wang comitted at
  27. c7dfa1c3 Make the syntax for la follow the convention of binders before body Anthony Wang authored at Anthony Wang comitted at
  28. fda117c1 Implement subtraction cause why not Anthony Wang authored at Anthony Wang comitted at
  29. 9edb84a8 Oops forgot to update dbtypes Anthony Wang authored at Anthony Wang comitted at
  30. 035781c7 Fix mul_comm proof, improve type checker speed and proof size by 2x! The specific killer optimization I implemented is to bundle fewer redundant types in the terms. I also improved the syntax of μLean slightly. Anthony Wang authored at Anthony Wang comitted at