42ab5dfab0
This PR makes two improvements to the local context when there are autobound implicits in `variable`s. First, the local context no longer has two copies of every variable (the local context is rebuilt if the types of autobound implicits have metavariables). Second, these metavariables get names using the same algorithm used by binders that appear in declarations (with `mkForallFVars'` instead of `mkForallFVars`). This removes the last use of `Term.addAutoBoundImplicits'`, which inherently has this variable duplication issue.
92 lines
1.8 KiB
Text
92 lines
1.8 KiB
Text
/-!
|
||
# Regression tests for auto-bound implicits
|
||
-/
|
||
|
||
set_option pp.mvars false
|
||
|
||
/-!
|
||
Auto-bound implicit appears in dot notation in the type, for a variable that appears later.
|
||
-/
|
||
example : n.succ = 1 → n = 0 := by
|
||
intros h; injection h
|
||
|
||
/-!
|
||
Auto-bound implicit appears in dot notation in a binder, for a variable that appears later.
|
||
-/
|
||
example (h : n.succ = 1) : n = 0 := by
|
||
injection h
|
||
|
||
/-!
|
||
Auto-bound implicit appears as argument to notation that is postponed.
|
||
The type of `σ` is specialized to `T` later.
|
||
-/
|
||
opaque T : Type
|
||
opaque T.Pred : T → T → Prop
|
||
|
||
example {ρ} (hρ : ρ.Pred σ) : T.Pred ρ ρ := sorry
|
||
|
||
|
||
namespace TestRunTermElab
|
||
/-!
|
||
In the following tests, there is an auto-bound implicit whose type is a metavariable,
|
||
which gets turned into an additional variable.
|
||
-/
|
||
|
||
def constUnit (a : A) : Type := Unit
|
||
|
||
/-!
|
||
The auto-bound implicit creates a new variable `A✝`, which comes from the argument name in `constUnit`.
|
||
(This has been the case well before the creation of this test.)
|
||
-/
|
||
/--
|
||
info: A✝ : Sort u_1
|
||
a : A✝
|
||
_x : constUnit a
|
||
⊢ True
|
||
-/
|
||
#guard_msgs in
|
||
example (_x : constUnit a) : True := by
|
||
trace_state
|
||
trivial
|
||
|
||
variable (x : constUnit a)
|
||
|
||
/-!
|
||
The local context here used to be
|
||
```
|
||
a✝ : ?_
|
||
x✝¹ : constUnit a✝
|
||
x✝ : Sort ?_
|
||
a : x✝
|
||
x : constUnit a
|
||
⊢ True
|
||
```
|
||
Note the duplication and `x✝` for the name of the metavariable-as-a-variable.
|
||
The duplication was because `runTermElabM` wasn't resetting the local context.
|
||
The poor variable name was due to using `mkForallFVars` instead of `mkForallFVars'`.
|
||
-/
|
||
/--
|
||
info: A✝ : Sort _
|
||
a : A✝
|
||
x : constUnit a
|
||
⊢ True
|
||
-/
|
||
#guard_msgs in
|
||
example : True := by
|
||
trace_state
|
||
trivial
|
||
|
||
/-!
|
||
Checking that `#check` also has the improvement.
|
||
-/
|
||
/--
|
||
info: 1 : Nat
|
||
---
|
||
info: A✝ : Sort _
|
||
a : A✝
|
||
x : constUnit a
|
||
⊢ ?_
|
||
-/
|
||
#guard_msgs in #check (by trace_state; exact 1)
|
||
|
||
end TestRunTermElab
|