Recommendatins for writing `do` like DSL

Stream: new members

[Markus Schmaus]

I have an idea for a DSL similar to the do notation that I want to explore.

Does anyone have any tips on writing a DSL in general?

Where can I find the components for the do notation in the source code? I found docs#Lean.Parser.Term.do, but that's just for parsing, and I can't find where this is connected with actual computation.

Thanks for your help.

[Sebastian Ullrich]

Are you aware of https://lean-lang.org/papers/do.pdf?

[Markus Schmaus]

I am aware and I am in the process of reading it, it's awesome.