Invalid parser

Stream: lean4

[Marcus Rossel]

The following code produces an error on the last line:

declare_syntax_cat map_field
declare_syntax_cat map_row

syntax map_field+ "\n" : map_row -- invalid parser 'map_row_', invalid empty symbol

Without the "\n" it doesn't produce an error.
I'm trying to define the parser in such a way that it parses one or more instances of a map field followed by a newline.
Is there some named parser for newlines, or how can I achieve this behaviour?

[Mac]

@Marcus Rossel

syntax map_field+ linebreak : map_row

[Marcus Rossel]

Is there a list of these kinds of general purpose parsers somewhere? I've seen things like colGt before and just have no clue what they are :big_smile:

[Mac]

@Marcus Rossel Ctrl+F/grep in the lean4 repo is your friend :wink: There is also a big list of the registered parser aliases in [Lean.Parser(https://github.com/leanprover/lean4/blob/efa2ded2249ed53ac8b96d3a70cf5e8329d53a45/src/Lean/Parser.lean#L21-L43) and you can look in folder itself for the listings of all the various parsers the Lean core uses.

I don't think there is currently any pretty documentation of this kind of stuff, though.

[Horatiu Cheval]

Does colGt stand for "column greater than"? My guess is that it's used for indentation based syntax, as in

syntax (name := myIntro) "myIntro " (colGt ident)? : tactic
macro_rules
| `(tactic| myIntro $e) => `(tactic| intro $e)

Then this works

example : p → p := by
  myIntro
    h

But this gives an error

example : p → p := by
  myIntro
 h

[Marcus Rossel]

@Mac Thanks! I'm guessing I'd have to grep for declare_syntax_cat right?

[Mac]

@Marcus Rossel no, I was suggesting you to grep for specific parsers (like colGt). If you just want to find what parsers are available, you should just read through the Lean/Parser folder. Every file in there defines tons of different parsers (the most basic ones being defined in Lean.Parser.Basic).

[Marcus Rossel]

(deleted)