Zulip Chat Archive

Stream: lean4

Topic: ParserDescr vs. Parser


Mac (May 18 2021 at 00:02):

In trying to teach myself to understand the Lean source code, I am trying to figure out the purpose of ParserDescr. From what I can tell, a ParserDescr is a utility object generated by the syntax DSL to summarize the essence of a grammar so that, in addition to a Parser, things like a Parenthesizer can be generated from the specification. Is this right? Or is there some more important distinction between Parser and ParserDescr that I am missing?


Last updated: Dec 20 2023 at 11:08 UTC