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.
167 lines
3.7 KiB
Text
167 lines
3.7 KiB
Text
/-!
|
||
# Changing variable binder annotations
|
||
|
||
Tests the use of the `variable` command to update the binder annotations of existing variables. -/
|
||
|
||
/-! Test updating between default and implicit annotations. -/
|
||
|
||
namespace Ex1
|
||
|
||
variable {α : Type}
|
||
variable [Add α]
|
||
variable (α)
|
||
def f (a : α) := a + a
|
||
/-- info: f Nat 5 : Nat -/
|
||
#guard_msgs in
|
||
#check f Nat 5
|
||
variable {α}
|
||
def g (b : α) := b
|
||
/-- info: g 5 : Nat -/
|
||
#guard_msgs in
|
||
#check g 5
|
||
/-- info: Ex1.f (α : Type) [Add α] (a : α) : α -/
|
||
#guard_msgs in
|
||
#check f
|
||
/-- info: Ex1.g {α : Type} (b : α) : α -/
|
||
#guard_msgs in
|
||
#check g
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
|
||
variable {α β : Type}
|
||
variable (α)
|
||
def f (a : α) := a
|
||
def g (b : β) := b
|
||
/-- info: f Nat 5 : Nat -/
|
||
#guard_msgs in
|
||
#check f Nat 5
|
||
/-- info: g 5 : Nat -/
|
||
#guard_msgs in
|
||
#check g 5
|
||
/-- info: Ex2.f (α : Type) (a : α) : α -/
|
||
#guard_msgs in
|
||
#check f
|
||
/-- info: Ex2.g {β : Type} (b : β) : β -/
|
||
#guard_msgs in
|
||
#check g
|
||
/-- error: redundant binder annotation update -/
|
||
#guard_msgs in
|
||
variable (α)
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
|
||
variable {α : Type}
|
||
variable (f : α → α)
|
||
variable (α)
|
||
def g (a : α) := f a
|
||
/-- info: Ex3.g (α : Type) (f : α → α) (a : α) : α -/
|
||
#guard_msgs in
|
||
#check g
|
||
variable {f}
|
||
def h (a : α) := f a
|
||
/-- info: Ex3.h (α : Type) {f : α → α} (a : α) : α -/
|
||
#guard_msgs in
|
||
#check h
|
||
end Ex3
|
||
|
||
namespace Ex4
|
||
|
||
variable {α β : Type}
|
||
variable (α γ)
|
||
def g (a : α) (b : β) (c : γ) := (a, b, c)
|
||
/-- info: g Nat Bool 10 "hello" true : Nat × String × Bool -/
|
||
#guard_msgs in
|
||
#check g Nat Bool 10 "hello" true
|
||
variable (f : α → α)
|
||
variable {f γ α}
|
||
def h (a : α) (c : γ) := (f a, c)
|
||
/-- info: Ex4.h.{u_1} {α : Type} {γ : Type u_1} {f : α → α} (a : α) (c : γ) : α × γ -/
|
||
#guard_msgs in
|
||
#check h
|
||
end Ex4
|
||
|
||
/-! Test updating from and to instance implicit. -/
|
||
|
||
namespace Ex5
|
||
|
||
variable [i : Add α]
|
||
variable (i)
|
||
def f (x y : α) := x + y
|
||
/-- info: Ex5.f.{u_1} {α : Type u_1} (i : Add α) (x y : α) : α -/
|
||
#guard_msgs in
|
||
#check f
|
||
variable [i]
|
||
def g (x y : α) := x + y
|
||
/-- info: Ex5.g.{u_1} {α : Type u_1} [i : Add α] (x y : α) : α -/
|
||
#guard_msgs in
|
||
#check g
|
||
end Ex5
|
||
|
||
/-! Test that variables with default values/tactics cannot be updated. -/
|
||
|
||
namespace Ex6
|
||
|
||
variable (a : Nat)
|
||
variable (h : a = a := rfl)
|
||
/-- error: cannot update binder annotation of variables with default values/tactics -/
|
||
#guard_msgs in
|
||
variable {h}
|
||
/-- error: cannot update binder annotation of variables with default values/tactics -/
|
||
#guard_msgs in
|
||
variable {a h}
|
||
def f := a
|
||
/-- info: Ex6.f (a : Nat) : Nat -/
|
||
#guard_msgs in
|
||
#check f
|
||
end Ex6
|
||
|
||
/-! Test that variables that cannot be instance implicit fail to be updated thereto. -/
|
||
|
||
namespace Ex7
|
||
|
||
variable (n : Nat)
|
||
/--
|
||
error: cannot update binder annotation of variable `n` to instance implicit:
|
||
invalid binder annotation, type is not a class instance
|
||
Nat
|
||
|
||
Note: Use the command `set_option checkBinderAnnotations false` to disable the check
|
||
-/
|
||
#guard_msgs in
|
||
variable [n]
|
||
variable (x)
|
||
/--
|
||
error: cannot update binder annotation of variable `x` to instance implicit:
|
||
variable was originally declared without an explicit type
|
||
-/
|
||
#guard_msgs in
|
||
variable [x]
|
||
end Ex7
|
||
|
||
/-! Test updating to and from strict implicit annotations. -/
|
||
|
||
namespace Ex8
|
||
|
||
variable {α : Type} (β γ : Type)
|
||
variable ⦃α⦄
|
||
def f (a : α) (_ : β) := a
|
||
/-- info: Ex8.f ⦃α : Type⦄ (β : Type) (a : α) : β → α -/
|
||
#guard_msgs in
|
||
#check f
|
||
variable (α) ⦃β γ⦄
|
||
def g (a : α) (b : β) (c : γ) := (a, b, c)
|
||
/-- info: Ex8.g (α : Type) ⦃β γ : Type⦄ (a : α) (b : β) (c : γ) : α × β × γ -/
|
||
#guard_msgs in
|
||
#check g
|
||
variable {β}
|
||
def h (b : β) := b
|
||
/-- info: Ex8.h {β : Type} (b : β) : β -/
|
||
#guard_msgs in
|
||
#check h
|
||
variable {{β}}
|
||
/-- error: redundant binder annotation update -/
|
||
#guard_msgs in
|
||
variable ⦃β⦄
|
||
end Ex8
|