Parser.trailingLoop

Stream: lean4

[Uranus Testing]

It looks like that this piece of code is not working anymore (modulo replacing combinatorFormatter with combinator_formatter and combinatorParenthesizer with combinator_parenthesizer, it reports expected ':'). It was working at the beggining of November, but I can’t figure out what changed (probably it is somehow related to this cache). Is it possible to write such parser now?

[Sebastian Ullrich]

The LHS is an improper term without precedence, this should have been broken long before November.

    let s := (leadingNode `foo maxPrec <| symbol "...").fn c s

[Uranus Testing]

Thanks, it works now.