Custom parser

Stream: lean4

[Björn Fischer]

Hi guys,

I'm trying to write a parser for alphanumerical names similar to @Sebastian Ullrich 's text parser. I copied it for the most part part, but I'm getting an error when I use it in my syntax.

def name : Parser := withAntiquot (mkAntiquot "name" `LX.text) {
  fn := fun c s =>
    let startPos := s.pos;
    let s := takeWhile1Fn (fun c => c.isAlphanum) "Invalid name" c s;
    mkNodeToken `LX.text startPos c s
}
syntax "pql!" name (labelmatcher)? : term

The error is

don't know how to generate formatter for non-definition '{ info :=
    { collectTokens := id, collectKinds := id, firstTokens := FirstTokens.unknown },
  fn := fun c s =>
    let startPos := s.pos;
    let s := takeWhile1Fn (fun c => Char.isAlphanum c) "Invalid name" c s;
    mkNodeToken `LX.text startPos c s }'

The stringLit parser works fine

syntax "pql!" strLit (labelmatcher)? : term

What does the error mean?

[Björn Fischer]

I'm on leanprover/lean4:v4.0.0-m4

[Sebastian Ullrich]

The full definition of the parser is at https://github.com/leanprover/lean4/blob/3e83e28e8f7a81931ef4d6c77b797a60fcfdf5a3/tests/playground/webserver/Webserver.lean#L100-L108, though other parts of that file would need to be updated for current Lean versions