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: May 02 2025 at 03:31 UTC