1. Top
  2. miscelleaneous
  3. Commits
miscelleaneous

Random Lean experiments

Commits at main

  1. 0e74df00 Update Lean to v4.33.0-rc2 Anthony Wang authored at Anthony Wang comitted at
  2. 5338c23f Update Lean to v4.33.0-rc1 Anthony Wang authored at Anthony Wang comitted at
  3. 32c78a5e Update Lean to v4.32.0 Anthony Wang authored at Anthony Wang comitted at
  4. b5838052 Add minimal #count_heartbeats import, fix Invariant.withEarlyReturn error Anthony Wang authored at Anthony Wang comitted at
  5. 4f5689f0 Update Lean to v4.32.0-rc1 Anthony Wang authored at Anthony Wang comitted at
  6. 47a9c994 Update Lean to v4.31.0 Anthony Wang authored at Anthony Wang comitted at
  7. 37825d5e Replace removed datetime function in CommitGraph.lean Anthony Wang authored at Anthony Wang comitted at
  8. eb6b9dd9 Update Lean to v4.31.0-rc2 Anthony Wang authored at Anthony Wang comitted at
  9. 52afbcda Messing around with implemented_by Anthony Wang authored at Anthony Wang comitted at
  10. 1c4ed2ae Delete duplicate first attempt at STLC Anthony Wang authored at Anthony Wang comitted at
  11. d76746ca Try out new range syntax Anthony Wang authored at Anthony Wang comitted at
  12. 9ba7109d Delete empty Category.lean file (I already have way too many files in this repo 😆) Anthony Wang authored at Anthony Wang comitted at
  13. 949cd9c2 Update Lean to v4.31.0-rc1 Anthony Wang authored at Anthony Wang comitted at
  14. 1da1ce9f Update Lean to v4.30.0 Anthony Wang authored at Anthony Wang comitted at
  15. 52c8e668 μKanren Anthony Wang authored at Anthony Wang comitted at
  16. 0a5da75c Messing around with attributes Anthony Wang authored at Anthony Wang comitted at
  17. be8d0abb More mvcgen fun I'm collecting cute mvcgen proofs Anthony Wang authored at Anthony Wang comitted at
  18. ebf9f3d5 Adjust formatting Anthony Wang authored at Anthony Wang comitted at
  19. c23185c5 Implement and prove the same optimization in STLC that I used in InfantLean Anthony Wang authored at Anthony Wang comitted at
  20. ff7d93c0 Cute gensym proof that I deleted from my other project Anthony Wang authored at Anthony Wang comitted at
  21. 3b740464 Bundle fewer types in terms which simplifies things a lot Anthony Wang authored at Anthony Wang comitted at
  22. 0d4ad641 Delete scratchpad stuff in Main.lean Anthony Wang authored at Anthony Wang comitted at
  23. e4f892bc Oops that's embarrassing Anthony Wang authored at Anthony Wang comitted at
  24. 278b8701 Leave STLC termination as a TODO since Harmonic's Aristotle gave up twice Anthony Wang authored at Anthony Wang comitted at
  25. db6f63f0 Add STLC.lean (finished except for strong normalization proof), fix LambCalc.lean mistakes Anthony Wang authored at Anthony Wang comitted at
  26. 6f94b219 Remove extra space Anthony Wang authored at Anthony Wang comitted at
  27. b2ece84a partial instead of unsafe for nontermination Anthony Wang authored at Anthony Wang comitted at
  28. 5ce6a815 Update Lean to v4.30.0-rc2 Anthony Wang authored at Anthony Wang comitted at
  29. 168c4741 Update Lean to v4.30-rc1 Anthony Wang authored at Anthony Wang comitted at
  30. 97cf6ffd Update Lean to v4.29.0 Anthony Wang authored at Anthony Wang comitted at