Commit 2024-09-09 19:54 1fa672e9

View on Github →

chore(Filter/Basic): use abbrev (#16624) Otherwise coframeMinimalAxioms.toCompleteLattice = instCompleteLatticeFilter isn't with_reducible_and_instances rfl.

Estimated changes