Explanation of the Lean 3 version is here (mostly about the top level).
Port https://github.com/madvorak/grammars/ to Lean 4