Commit 2023-05-28 21:54 4bf88e01
View on Github →chore: forward-port leanprover-community/mathlib#19081 (#4399)
This PR also uncomment assert_not_exists which was forgotten to be uncommented when assert_not_exists was ported.
chore: forward-port leanprover-community/mathlib#19081 (#4399)
This PR also uncomment assert_not_exists which was forgotten to be uncommented when assert_not_exists was ported.