Pervognsen recommends Lean's approach to self-extensible parsing
3Nov 1 1:22 PM · 10d ago · 1 comment · 1 source · development 3 of 8
A Lobsters commenter points to Lean's implementation of Pratt parsing in self-extensible languages, noting how dependent typing forces single-pass execution with natural synchronization boundaries.
Nov 2Nov 3Nov 4Nov 5Nov 6Nov 7Nov 8Nov 9yesterdaynow · 7:42 PM ET
What people said 1 voice · verbatim
P
For Pratt parsing as a component of a self-extensible language like this, it's worth checking out what Lean does. Most dependently typed languages require explicit forward declarations and other things that already force them to run in a single pass at the top level. In Lean's case, the top-level granularity is one command-like item executed in a…
