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.
66 lines
1.2 KiB
Lean4
66 lines
1.2 KiB
Lean4
import Lean
|
|
/-!
|
|
# Make sure generated instance names are unique if there are macro scopes
|
|
-/
|
|
|
|
open Lean Elab Command
|
|
|
|
/-!
|
|
Example adapted from #2044
|
|
-/
|
|
|
|
#eval (do
|
|
let stx ← `(
|
|
structure Foo where
|
|
field : String
|
|
instance : Nonempty Foo := ⟨⟨"hi"⟩⟩)
|
|
elabCommand stx
|
|
: CommandElabM Unit
|
|
)
|
|
|
|
/-- error: Unknown identifier `instNonemptyFoo` -/
|
|
#guard_msgs in #check instNonemptyFoo
|
|
|
|
-- Verify that `instNonemptyFoo` is the name it would generate if it weren't hygienic
|
|
|
|
structure Foo where
|
|
field : String
|
|
instance : Nonempty Foo := ⟨⟨"hi"⟩⟩
|
|
|
|
/-- info: instNonemptyFoo : Nonempty Foo -/
|
|
#guard_msgs in #check instNonemptyFoo
|
|
|
|
/-!
|
|
Example directly from #2044, deriving ToJson
|
|
-/
|
|
|
|
open Lean Elab Command
|
|
#eval (do
|
|
let stx ← `(
|
|
structure Foo where
|
|
field : String
|
|
deriving ToJson)
|
|
elabCommand stx
|
|
: CommandElabM Unit
|
|
)
|
|
/-- error: Unknown identifier `instToJsonFoo` -/
|
|
#guard_msgs in #check instToJsonFoo
|
|
|
|
deriving instance ToJson for Foo
|
|
|
|
/-- info: instToJsonFoo : ToJson Foo -/
|
|
#guard_msgs in #check instToJsonFoo
|
|
|
|
|
|
/-!
|
|
Can derive RpcEncodable multiple times in the same namespace.
|
|
-/
|
|
|
|
structure A1 where
|
|
n : Nat
|
|
deriving Lean.Server.RpcEncodable
|
|
|
|
structure A2 where
|
|
n : Nat
|
|
deriving Lean.Server.RpcEncodable
|