mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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.
105 lines
3.1 KiB
Lean4
105 lines
3.1 KiB
Lean4
/-!
|
||
# Dot notation and CoeFun
|
||
|
||
https://github.com/leanprover/lean4/issues/1910
|
||
-/
|
||
|
||
set_option pp.mvars false
|
||
|
||
/-!
|
||
Test that dot notation resolution can see through CoeFun instances.
|
||
-/
|
||
|
||
structure Equiv (α β : Sort _) where
|
||
toFun : α → β
|
||
invFun : β → α
|
||
|
||
infixl:25 " ≃ " => Equiv
|
||
|
||
instance : CoeFun (α ≃ β) fun _ => α → β where
|
||
coe := Equiv.toFun
|
||
|
||
structure Foo where
|
||
n : Nat
|
||
|
||
def Foo.n' : Foo ≃ Nat := ⟨Foo.n, Foo.mk⟩
|
||
|
||
variable (f : Foo)
|
||
/-- info: Foo.n'.toFun f : Nat -/
|
||
#guard_msgs in #check f.n'
|
||
|
||
example (f : Foo) : f.n' = f.n := rfl
|
||
|
||
/-!
|
||
Fail dot notation if it requires using a named argument from the CoeFun instance.
|
||
-/
|
||
structure F where
|
||
f : Bool → Nat → Nat
|
||
|
||
instance : CoeFun F (fun _ => (x : Bool) → (y : Nat) → Nat) where
|
||
coe x := fun (a : Bool) (b : Nat) => x.f a b
|
||
|
||
-- Recall CoeFun oddity: it uses the unfolded *value* to figure out parameter names.
|
||
-- That's why this is `a` and `b` rather than `x` and `y`.
|
||
/-- info: fun x => (fun a b => x.f a b) true 2 : F → Nat -/
|
||
#guard_msgs in #check fun (x : F) => x (a := true) (b := 2)
|
||
|
||
def Nat.foo : F := { f := fun _ b => b }
|
||
|
||
-- Ok:
|
||
/-- info: fun n x => (fun a b => Nat.foo.f a b) x n : Nat → Bool → Nat -/
|
||
#guard_msgs in #check fun (n : Nat) => (Nat.foo · n)
|
||
|
||
-- Intentionally fails:
|
||
/--
|
||
error: Invalid field notation: `Nat.foo.f` (coerced from `Nat.foo`) has a parameter with expected type
|
||
Nat
|
||
but it cannot be used
|
||
|
||
Note: Field notation cannot refer to parameter `b` by name because that constant was coerced to a function
|
||
|
||
Hint: Consider rewriting this application without field notation (e.g., `C.f x` instead of `x.f`)
|
||
---
|
||
info: fun n => sorry : (n : Nat) → ?_ n
|
||
-/
|
||
#guard_msgs in #check fun (n : Nat) => n.foo
|
||
|
||
/-!
|
||
Make sure that dot notation does not use the wrong CoeFun instance.
|
||
The following instances rely on the second one having higher priority,
|
||
so we need to fail completely when the instances would depend on argument values.
|
||
-/
|
||
|
||
structure Bar (b : Bool) where
|
||
|
||
instance : CoeFun (Bar b) (fun _ => Bar b → Bool) where
|
||
coe := fun _ _ => b
|
||
|
||
instance : CoeFun (Bar true) (fun _ => (b : Bool) → Bar b) where
|
||
coe := fun _ _ => {}
|
||
|
||
def Bar.bar : Bar true := {}
|
||
|
||
/-- info: fun f => (fun x => false) f : Bar false → Bool -/
|
||
#guard_msgs in #check fun (f : Bar false) => Bar.bar false f
|
||
/--
|
||
error: Invalid field notation: Function `Bar.mk` (coerced from `Bar.bar`) does not have a usable parameter of type `Bar ...` for which to substitute `f`
|
||
|
||
Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation
|
||
---
|
||
info: fun f => sorry : (f : Bar false) → ?_ f
|
||
-/
|
||
#guard_msgs in
|
||
#check fun (f : Bar false) => f.bar false
|
||
|
||
/-- info: fun f => (fun x => false) f : Bar false → Bool -/
|
||
#guard_msgs in #check fun (f : Bar false) => Bar.bar true false f
|
||
/--
|
||
error: Invalid field notation: Function `Bar.mk` (coerced from `Bar.bar`) does not have a usable parameter of type `Bar ...` for which to substitute `f`
|
||
|
||
Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation
|
||
---
|
||
info: fun f => sorry : (f : Bar false) → ?_ f
|
||
-/
|
||
#guard_msgs in #check fun (f : Bar false) => f.bar true false
|