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

Cryptography final project

Commits at main

  1. c6abf744 Oops forgot to serialize unit_rec Anthony Wang authored at Anthony Wang comitted at
  2. f1c8b8e7 Update to Lean v4.31.0-rc1 Anthony Wang authored at Anthony Wang comitted at
  3. 6f73f4e5 Use toTypeExpr instead of manually constructing the exprs Anthony Wang authored at Anthony Wang comitted at
  4. 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
  5. fd2b9342 Crazy fun metaprogramming to autogenerate list of defs Anthony Wang authored at Anthony Wang comitted at
  6. b7c7b7ac Add unit_rec, support equality of types Anthony Wang authored at Anthony Wang comitted at
  7. b6f3134f Only 1500 (non-blank) lines now! Anthony Wang authored at Anthony Wang comitted at
  8. 3d419899 More tactics Anthony Wang authored at Anthony Wang comitted at
  9. 69078955 Merge pull request #1 from i-love-lean/add-macrolean Reorganize into microlean/ + macrolean/ i-love-lean authored at GitHub comitted at
  10. 6b8c2961 Use array instead of list Anthony Wang authored at Anthony Wang comitted at
  11. 64da70e0 Fix typos Anthony Wang authored at Anthony Wang comitted at
  12. 8ecccea8 Use OfNat typeclass for less jankiness Anthony Wang authored at Anthony Wang comitted at
  13. 8e8358a5 New clc tactic and better notation for type of Anthony Wang authored at Anthony Wang comitted at
  14. 36d802f5 Don't allow earlier defs to depend on later ones Anthony Wang authored at Anthony Wang comitted at
  15. 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
  16. 88731c6c add_comm ZKP example Anthony Wang authored at Anthony Wang comitted at
  17. 5f4c48ff Commit more slop Dan Klishch authored at Dan Klishch comitted at
  18. f720cd1a Update dbtypes Anthony Wang authored at Anthony Wang comitted at
  19. aa5a45f0 Better formatting for test output Anthony Wang authored at Anthony Wang comitted at
  20. 61d48690 Delete unused slop lemmas Anthony Wang authored at Anthony Wang comitted at
  21. 3b1e66a0 Technically not an elaborator Anthony Wang authored at Anthony Wang comitted at
  22. 2ef76866 More comments, rearrange some stuff Anthony Wang authored at Anthony Wang comitted at
  23. ddce1e73 SQRT 2 IS IRRATIONAL I also made the elaborator 5x faster yay Anthony Wang authored at Anthony Wang comitted at
  24. 052a7f67 Make the type checker 50x faster, some progress towards √2 irrational Anthony Wang authored at Anthony Wang comitted at
  25. 142d8bf6 INFINITE UNIVERSES (necessary for succ_ne_zero) Anthony Wang authored at Anthony Wang comitted at
  26. 467ad16e Move apb apr const to a more logical place Anthony Wang authored at Anthony Wang comitted at
  27. 05f5f38f Fix typos Anthony Wang authored at Anthony Wang comitted at
  28. c7dfa1c3 Make the syntax for la follow the convention of binders before body Anthony Wang authored at Anthony Wang comitted at
  29. fda117c1 Implement subtraction cause why not Anthony Wang authored at Anthony Wang comitted at
  30. 9edb84a8 Oops forgot to update dbtypes Anthony Wang authored at Anthony Wang comitted at