1. Top
  2. evolution
  3. Commits
evolution

The evolution of a Lean programmer

Commits at d5586c201a40ad7f70db27ea5be9d8f9531991c8

  1. d5586c20 Revert "Don't need to return in identity monad" This reverts commit 9baf7fc0daca8a230f11512125ef663a5d60f801. Anthony Wang authored at Anthony Wang comitted at
  2. 4749b919 Oh don't need to import Std apparently Anthony Wang authored at Anthony Wang comitted at
  3. 9baf7fc0 Don't need to return in identity monad Anthony Wang authored at Anthony Wang comitted at
  4. dc79ca7f Add CC BY-SA license It's a bit weird to license code using that but it's the exact same code (well, nearly) as my blog post which is under CC BY-SA Anthony Wang authored at Anthony Wang comitted at
  5. 6dcc06d7 More fun with cat emojis Anthony Wang authored at Anthony Wang comitted at
  6. 6cdeba48 List.Perm is redundant Anthony Wang authored at Anthony Wang comitted at
  7. f13dc69c Don't need to abbrev when already @[simp]ed Anthony Wang authored at Anthony Wang comitted at
  8. 42eb7d85 Completely vibecoded solution, better golf, enlightened sort, make grind default tactic for SortedRange Anthony Wang authored at Anthony Wang comitted at
  9. f089fdc9 Don't need the names of invariant cases Anthony Wang authored at Anthony Wang comitted at
  10. 9ebe5846 Oh how could I forget about native_decide Anthony Wang authored at Anthony Wang comitted at
  11. a4b7906e Nuke README Anthony Wang authored at Anthony Wang comitted at
  12. 40e05cc5 Note that AristotleLemmas section is AI-generated Anthony Wang authored at Anthony Wang comitted at
  13. 7baa176d More consistency Anthony Wang authored at Anthony Wang comitted at
  14. ae0439d7 It's not that long... Anthony Wang authored at Anthony Wang comitted at
  15. b79c2fa7 Finished! Anthony Wang authored at Anthony Wang comitted at
  16. 9eaa66e2 Initial commit Anthony Wang authored at Anthony Wang comitted at