Commit 2024-03-23 19:34 76e46f2e

View on Github →

chore: fix some @[ext] attribute (#11494) This PR contains 2 changes:

  1. Order/Interval.lean: Add @[ext (flat := false)], which addressed the porting notes.
  2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in https://github.com/leanprover/std4/pull/159).
  3. Algebra/Order/Interval.lean updated now that ext_iff's namespace is changed due to 1. Partially addresses #11182

Estimated changes

deleted theorem Matrix.ext'
deleted theorem NonemptyInterval.ext
deleted theorem NonemptyInterval.ext_iff