655ec964f5
Given
```lean
structure A where
x : Nat
structure B extends A where
y : Nat
```
rather than pretty printing `{ x := 1, y := 2 : B }` as `{ toA := { x :=
1 }, y := 2 }`, it now pretty prints as `{ x := 1, y := 2 }`.
The option `pp.structureInstances.flatten` controls whether to flatten
structure instances like this.
|
||
|---|---|---|
| .. | ||
| Delaborator | ||
| Basic.lean | ||
| Delaborator.lean | ||
| Formatter.lean | ||
| Parenthesizer.lean | ||