Brendan Zabarauskas on Twitter: "@jcreed @edwinbrady I think Lean 4 has something like this too now! https://t.co/SPllX2Yshj" / Twitter

props to

for having a feature in idris for quite a few years (!-notation) I have wanted something like forever, and somehow I never heard about it till now.

Quote Tweet

Replying to @jcreed and @bubblingbeebles

Have you seen @whyevernoso's proposal, github.com/ghc-proposals/? I thought it was very reasonable.

3

6

Replying to

and

I think Lean 4 has something like this too now! leanprover.github.io/lean4/doc/do.h

Conversation