Add support for "nested actions"? #6919
magnus-madsen
started this conversation in
Ideas
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Add support for an alternative implicit monadic syntax (to complement
forM
).See https://lean-lang.org/functional_programming_in_lean/hello-world/conveniences.html#nested-actions
We cannot use
do
because it already has another meaning, but assuming we overloadforM
the idea would that:can also be written as
Another, perhaps better, example:
Beta Was this translation helpful? Give feedback.
All reactions