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.