08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
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
|
||
intro 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.)
|
||
-/
|
||
/--
|
||
trace: 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'`.
|
||
-/
|
||
/--
|
||
trace: 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
|
||
---
|
||
trace: A✝ : Sort _
|
||
a : A✝
|
||
x : constUnit a
|
||
⊢ ?_
|
||
-/
|
||
#guard_msgs in #check (by trace_state; exact 1)
|
||
|
||
end TestRunTermElab
|