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