lean4
lean4 copied to clipboard
leanprover
feat: `pp.parens` option to pretty print with all parentheses
This was a feature in the Lean 3 community edition.
Right now this is over-parenthesizing expressions compared to the Lean 3 version. Before, numerals and identifiers were not parenthesized. (Example output)
@Kha What do you think about this implementation? Do you have any ideas how to make it not parenthesize atomic syntax? In particular, is there some condition that implies parentheses are never needed?
- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-20' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-21 01:57:36)
Perhaps something like (← read).forceParens && prec < maxPrec? That is, if the precedence of the thing to be parenthesized is already at least the precedence of parens, there is no need to do it.
@Kha I've tried a few variations on that, but they didn't seem to have any effect. I think I've spent my time budget on this feature -- maybe if it the basic version of the feature exists, someone who is keen on having it prettier will figure out a solution?