Genuinely, writing DSLs in Lean is so amazing; you literally get to define your own grammar like it feels like you're giving input to a parser generator, except, you don't have to write the error handling, you get syntax highlighting, etc. and it's all live updating in your current file!!!
yeah menhir is much nicer to use because it calls into the ocaml type checker and shows error messages in the menhir file, rather than dumping out errors that don't fit on your screen from a file you didn't write ^^
aside from that they're pretty comparable though. i think both have some features that the other doesn't but at least i've never really missed anything from one in the other
Comments
grammar MyLang where
expr := num | var | binop expr op expr
op := "+" | "*" | "-"