10a56bf4a1
The previous implementation was using the following heuristic
```lean
-- heuristic: use non-dependent arrows only if possible for whole group to avoid
-- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
let dependent := curNames.any fun n => hasIdent n.getId stxBody
```
The result produced by this heuristic was **not** producing an
accidental name capture, but I agree
it was confusing to have `∀ (a : True), ∃ a, a = a : Prop` instead of
`True → ∃ a, a = a : Prop` since there is no dependency.
AFAICT, all examples affected by this commit have a better output now.
cc @digma0 @kha
43 lines
906 B
Text
43 lines
906 B
Text
A.a' : ∀ (self : A), self.x = 1
|
|
z : A
|
|
this : z.x = 1
|
|
⊢ z.x = 1
|
|
z : A
|
|
this : z.x = 1
|
|
⊢ z.x = 1
|
|
@A.rec : {motive : A → Sort u_1} → ((x : Nat) → (a' : x = 1) → motive (A.mk x)) → (t : A) → motive t
|
|
z : A
|
|
x : Nat
|
|
a' : x = 1
|
|
⊢ (A.mk x).x = 1
|
|
case mk
|
|
x : Nat
|
|
a' : x = 1
|
|
⊢ (A.mk x).x = 1
|
|
case mk
|
|
x y : Nat
|
|
⊢ { x := x, y := y } = { x := { x := x, y := y }.x, y := { x := x, y := y }.y }
|
|
a.1 = 1
|
|
z : A
|
|
x✝ : Nat
|
|
h : x✝ = 1
|
|
⊢ (A.mk x✝).x = 1
|
|
z : A
|
|
x : Nat
|
|
a' : x = 1
|
|
⊢ (A.mk x).x = 1
|
|
autoIssue.lean:60:18-60:19: error: don't know how to synthesize placeholder
|
|
context:
|
|
⊢ 1 = 1
|
|
autoIssue.lean:63:9-63:10: error: don't know how to synthesize placeholder for argument 'a''
|
|
context:
|
|
⊢ 1 = 1
|
|
autoIssue.lean:68:6-68:7: error: don't know how to synthesize placeholder for argument 'h'
|
|
context:
|
|
⊢ 2 = 1
|
|
autoIssue.lean:72:2-72:6: error: unsolved goals
|
|
case h
|
|
⊢ ?x = 1
|
|
|
|
case x
|
|
⊢ Nat
|