## Stream: lean4

### Topic: Creating a DSL

#### Calvin Lee (Mar 20 2021 at 05:33):

Hi, are there any tips on creating a DSL? other than creating a new syntax kind? Is do notation defined anywhere that I can take a look at?

#### Julian Berman (Mar 20 2021 at 13:32):

Parser here and elaborator here it'd seem, if you haven't found those already.

#### Calvin Lee (May 05 2021 at 18:18):

Hello! I'm working on creating a DSL using macros.
I haven't programmed in lean for awhile though, so I have a bit of a silly question to start out with: how do you create a new syntax category?

#### Daniel Selsam (May 05 2021 at 18:27):

declare_syntax_cat mycat

syntax ident  : mycat
syntax "(" mycat ")" : mycat

syntax "to_term"  mycat : term

macro_rules
| (to_term $a:ident) => ($a)
| (to_term ($a)) => (to_term$a)

syntax "[mycat|" mycat "]" : term

macro_rules
| ([mycat| $m]) => (to_term$m)

#check [mycat| ((Nat.add))]


#### Calvin Lee (May 05 2021 at 18:34):

Is there any way I can make my DSL translate into the do DSL?
i.e. instead of term i would translate into the do category?

#### Mac (May 05 2021 at 18:38):

@Daniel Selsam fyi,toTerm! should probably be to_term to fit with the new Lean 4 naming conventions, correct? ! is now only supposed to be used for functions that panic (see https://github.com/leanprover/lean4/issues/406); macro keywords use snake case now (like nat_lit`) .

#### Calvin Lee (May 05 2021 at 19:41):

Is there any way to generate some identifier I can use that won't interfere with anything else?

#### Mario Carneiro (May 05 2021 at 20:45):

This is the default behavior if you use a variable name in a macro. This is called "macro hygiene" and is a major part of the lean 4 macro framework

Last updated: May 18 2021 at 23:14 UTC