f73eb1246a
When `pp.safe_shadowing` is set to true, we still use the
suggested name if the "body" does not contain a free variable with the
suggested name. This is the approach used in Lean 3, and I think it
improved the result in all affected tests.
The implementation was simple. The only nasty case was `delabAppMatch`.
The main motivation for this feature was hovering information such as
```lean
f : {α_1 : Type} → α_1 → α_1
```
when hovering over the `f` at
```lean
def g (α : Type) (a : α) :=
f a
```
With `safe_shadowing`, we get the nicer
```lean
f : {α : Type} → α → α
```
cc @Kha
26 lines
896 B
Text
26 lines
896 B
Text
id fun (x : ?m) => x : ?m → ?m
|
|
0 : Nat
|
|
f 1 fun (x : Nat) => x : Nat
|
|
0 : Nat
|
|
f 1 fun (x : Nat) => x : Nat
|
|
id : ?m → ?m
|
|
precissues.lean:15:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
|
|
id : ?m → ?m
|
|
precissues.lean:17:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
|
|
1 : Nat
|
|
id ((fun (this : True) => this) True.intro) : True
|
|
0 = (fun (this : Nat) => this) 1 : Prop
|
|
0 =
|
|
let x : Nat := 0;
|
|
x : Prop
|
|
p ↔ ¬q : Prop
|
|
True = ¬False : Prop
|
|
p ∧ ¬q : Prop
|
|
¬p ∧ q : Prop
|
|
¬p ↔ q : Prop
|
|
¬p = q : Prop
|
|
¬p = q : Prop
|
|
id ¬p : Prop
|
|
(a a : Nat) → a = a : Prop
|
|
id : ?m → ?m
|
|
precissues.lean:41:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
|