opened
jgroote
username_0
*Issue migrated from trac ticket # 1131*

**component:** Core: Print Library | **priority:** minor

#### 2013-02-14 22:17:46: @username_2 created the issue


___
Currently too many parentheses are used when printing abstractions in certain contexts. For example:

```
forall n: Bool. n => (forall k: Bool. k => n)
```

It looks like the function print_expression needs to be specialized for abstractions (and possibly some other operators too).
Unnecessary parentheses in pretty printing of abstractions
issue
created
tneele
username_1
I do not find the provided example very convincing. The precedence of the forall operator is lower than the implication operator (ie, the implication binds stronger. The fact that the `forall k` occurs on the right-hand side of the implication is essential for the fact that `forall n: Bool. n => forall k: Bool. k => n` can only be interpreted in one way.

However, commit 2f4a60ce74d43 introduced some new unnecessary parentheses. For example, in the expression `(a && a) && a`, the parentheses are not necessary.
comment
created
wiegerw
username_2
The change in commit 07bc09d should solve the unnecessary problem with parentheses in the expression `(a && a) && a`. Perhaps there are more operators with the wrong associativity annotations. The problem is that information about associativity is only partially available in the dparser grammar.
comment