Skip to content

[Merged by Bors] - chore: unsimp Set.coe_setOf#39582

Closed
plp127 wants to merge 12 commits into
leanprover-community:masterfrom
plp127:aliu/set-coe
Closed

[Merged by Bors] - chore: unsimp Set.coe_setOf#39582
plp127 wants to merge 12 commits into
leanprover-community:masterfrom
plp127:aliu/set-coe