Zulip Chat Archive

Stream: lean4

Topic: expected parser to return exactly one syntax object


Wojciech Nawrocki (Dec 31 2022 at 13:38):

I am seeing the following mysterious error when trying to use a Parser as the category in a quotation. Does anyone know what I am doing wrong?

import Lean
open Lean Parser

def cat : Parser := ident >> " = " >> termParser

syntax "cat: " cat : term
macro_rules
  -- works
  | `(term| cat: $_ = $b) => pure b

#check cat: foo = "abc" -- works

/- expected parser to return exactly one syntax object -/
#check `(cat| foo = "abc")

Wojciech Nawrocki (Dec 31 2022 at 14:53):

It looks like it works if I define a new category instead. Should parsers not be used as categories? If they can, perhaps it's not always okay?

declare_syntax_cat catter
syntax ident " = " term : catter

#check `(catter| foo = "abc") -- works

Last updated: Dec 20 2023 at 11:08 UTC