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.
36 lines
1006 B
Lean4
36 lines
1006 B
Lean4
import Lean.Meta
|
|
/-!
|
|
This test checks that within ```realizeConst ``foo `foo.test``` we are not restricted
|
|
to adding declarations with a name scoped under `foo`, but can add any names
|
|
to the environment. This is important for constructions that add names to each
|
|
function in a mutual recursive group.
|
|
-/
|
|
def foo := True
|
|
def bar := True
|
|
|
|
open Lean Meta
|
|
|
|
-- NOTE: declaring and running a `realizeConst` invocation isn't usually done in the same file, so
|
|
-- changing the closure below may require a server restart to see the changes.
|
|
|
|
run_meta do
|
|
realizeConst ``foo `foo.test do
|
|
addDecl <| Declaration.thmDecl {
|
|
name := `foo.test
|
|
type := mkConst ``True
|
|
value := mkConst ``True.intro
|
|
levelParams := [] }
|
|
addDecl <| Declaration.thmDecl {
|
|
name := `bar.test
|
|
type := mkConst ``True
|
|
value := mkConst ``True.intro
|
|
levelParams := [] }
|
|
|
|
/-- info: foo.test : True -/
|
|
#guard_msgs in
|
|
#check foo.test
|
|
|
|
/-- info: bar.test : True -/
|
|
#guard_msgs in
|
|
#check bar.test
|