Commit 2023-11-15 00:39 65ff2214

feat: make Set.monad not an instance and add (Subtype.val '' ·) coercion (#8413) The monad instance on Set isn't computationally relevant, and it causes Lean's monad lifting coercion logic to activate. We introduce a coercion instance for the case that's actually used in practice: when s : Set X and t : Set s then (t : Set X) ought to be Subtype.val '' t. This way we do not see Lean.Internal.coeM terms. If the monad is still wanted, it can be activated using a local attribute or by using the SetM.run function.