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.
109 lines
2.6 KiB
Lean4
109 lines
2.6 KiB
Lean4
/-!
|
||
# Tests for generalized field notation through aliases and "top-level" dot notation
|
||
https://github.com/leanprover/lean4/issues/3031
|
||
-/
|
||
|
||
/-!
|
||
Alias dot notation. There used to be a different kind of alias dot notation;
|
||
in the following example, it would have looked for an argument of type `Common.String`.
|
||
Now it looks for one of type `String`, allowing libraries to add "extension methods" from within their own namespaces.
|
||
-/
|
||
def Common.String.a (s : String) : Nat := s.length
|
||
|
||
export Common (String.a)
|
||
|
||
/-- info: String.a "x" : Nat -/
|
||
#guard_msgs in #check String.a "x"
|
||
/-- info: String.a "x" : Nat -/
|
||
#guard_msgs in #check "x".a
|
||
|
||
/-!
|
||
Declarations take precedence over aliases
|
||
-/
|
||
def String.a (s : String) : Nat := s.length + 100
|
||
/-- info: "x".a : Nat -/
|
||
#guard_msgs in #check "x".a
|
||
/-- info: 100 -/
|
||
#guard_msgs in #eval "".a
|
||
|
||
/-!
|
||
Private declarations take precedence over aliases
|
||
-/
|
||
private def String.b (s : String) : Nat := 0
|
||
def Common.String.b (s : String) : Nat := 1
|
||
export Common (String.b)
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval "".b
|
||
|
||
/-!
|
||
Multiple aliases is an error
|
||
-/
|
||
def Common.String.c (s : String) : Nat := 0
|
||
def Common'.String.c (s : String) : Nat := 0
|
||
export Common (String.c)
|
||
export Common' (String.c)
|
||
/--
|
||
error: Field name `c` is ambiguous: `String.c` has possible interpretations `Common'.String.c`, `Common.String.c`
|
||
-/
|
||
#guard_msgs in #eval "".c
|
||
|
||
/-!
|
||
Aliases work with inheritance
|
||
-/
|
||
namespace Ex1
|
||
structure A
|
||
structure B extends A
|
||
def Common.A.x (_ : A) : Nat := 0
|
||
export Common (A.x)
|
||
/-- info: fun b => A.x b.toA : B → Nat -/
|
||
#guard_msgs in #check fun (b : B) => b.x
|
||
end Ex1
|
||
|
||
/-!
|
||
`open` also works
|
||
-/
|
||
def Common.String.parse (_ : String) : List Nat := []
|
||
|
||
namespace ExOpen1
|
||
/--
|
||
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
|
||
""
|
||
of type `String`
|
||
-/
|
||
#guard_msgs in #check "".parse
|
||
section
|
||
open Common
|
||
/-- info: String.parse "" : List Nat -/
|
||
#guard_msgs in #check "".parse
|
||
end
|
||
section
|
||
open Common (String.parse)
|
||
/-- info: String.parse "" : List Nat -/
|
||
#guard_msgs in #check "".parse
|
||
end
|
||
end ExOpen1
|
||
|
||
|
||
namespace Ex2
|
||
class A (n : Nat) where
|
||
x : Nat
|
||
|
||
/-!
|
||
Incidental fix: `@` for generalized field notation was failing if there were implicit arguments.
|
||
True projections were ok.
|
||
-/
|
||
def A.x' {n : Nat} (a : A n) := a.x
|
||
|
||
/-- info: fun a => a.x' : A 2 → Nat -/
|
||
#guard_msgs in #check fun (a : A 2) => @a.x'
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
variable (f : α → β) (g : β → γ)
|
||
/-!
|
||
Functions use the "top-level" dot notation rule: they use the first explicit argument, rather than the first function argument.
|
||
-/
|
||
/-- info: g ∘ f : α → γ -/
|
||
#guard_msgs in #check g.comp f
|
||
end Ex3
|