This package slightly refactors and extends the user interface of Robin Arnez's experimental Lean 4 parser tracing framework, lean4#13792. See Examples.lean for what is added.

The Lean 4 category parser prefers longest matches above anything else, even if those end up in error states. That can lead to surprising behavior; an instance of this was brought up here and discussed in the subsequent 2026-05-13 Meta Café. After that, Robin decided to implement the parser tracing framework.

LongestMatches.lean contains an elucidation of the matter, using minimal examples.

Instead of the original toolchain from lean4#13792, this project uses a more recent toolchain from https://github.com/whxvd/lean4 that includes the PR.