jason reed@jcreed·Aug 20, 2021props to @edwinbrady 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 Tweetshachaf@shachaf · Aug 20, 2021Replying to @jcreed and @bubblingbeeblesHave you seen @whyevernoso's proposal, https://github.com/ghc-proposals/ghc-proposals/pull/64…? I thought it was very reasonable.36
Brendan Zabarauskas@brendanzabReplying to @jcreed and @edwinbradyI think Lean 4 has something like this too now! https://leanprover.github.io/lean4/doc/do.html#nested-actions…12:22 AM · Aug 21, 2021·Twitter Web App2 Likes