Consider inverting sense of parenthesis-style directive ParoundPrec

[mn200]

Currently the documentation says:

The ParoundPrec value [...] causes parentheses to be added when the term is the argument to a function with a different precedence level.

The code implements this, but this feature is not used in the HOL distribution at all. I think it might be useful if it was inverted, so that parentheses were inserted if the context had the same precedence level. This could be used to force parenthesisation of fancy suffixes, such as ⁻¹, which stacks awkwardly, as in:

> load "realLib";
val it = (): unit
> ``inv (inv 2)``;
val it = “2⁻¹ ⁻¹”: term

The theory of relations is full of different suffixes at the same precedence level, so it would make most sense to parenthesise at the same level (rather than keying off the name), giving us things like “(R⁺)ᵀ” rather than “R⁺ ᵀ”. Another alternative would be to allow the superscript characters to merge (making them non-aggregating, like (, ), [, ] and ~), so the term would print as “R⁺ᵀ”. However, I think that last choice is actually rather confusing.

This same change would also make the following look better:

> ``(x ** 2) ** 3``;
val it = “x² ³”: term

[binghe]

I support the first idea. The "alternative" may cause (x ** 2) ** 3 being printed as “x²³” which is even more confusing than “R⁺ᵀ”

[mn200]

Absolutely. Of course, if the "alternative" were pursued, not all superscripts would have to be made non-aggregating, and the numeral superscripts would have to stay as they are. We would have to put up with “x² ³”. All in all, I'm much more in favour of the original idea.