Commit 2024-01-01 19:29 5192777c

View on Github →

refactor: decapitalize names in @[mk_iff] (#9378)

  • @[mk_iff] class MyPred now generates myPred_iff, not MyPred_iff
  • add Lean.Name.decapitalize
  • fix indentation and a few typos in the docs/comments. Partially addresses issue #9129

Estimated changes

modified theorem Multiset.rel_zero_left
modified theorem Multiset.rel_zero_right