Commit 2024-10-30 01:08 ebecc123

View on Github →

chore: remove a Monad assumption and a linked do (#18420) #17715 and see also this Zulip discussion. Note that removing just the Monad m assumption would disallow do-notation in the following definition. However, removing both is allowed, since do is only used in elaboration, but does not appear in the final type.

Estimated changes