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.
64 lines
1022 B
Lean4
64 lines
1022 B
Lean4
|
||
|
||
namespace Foo
|
||
|
||
protected def x := 10
|
||
|
||
end Foo
|
||
|
||
open Foo
|
||
#check x -- error unknown identifier `x`
|
||
|
||
#check Foo.x
|
||
|
||
namespace Bla.Foo
|
||
protected def y := 20
|
||
def z := 30
|
||
end Bla.Foo
|
||
|
||
open Bla
|
||
#check Foo.y
|
||
open Bla.Foo
|
||
#check y -- error unknown identifier `y`
|
||
#check z
|
||
|
||
protected def x := 0 -- Error
|
||
|
||
protected partial def Foo.f (x : Nat) :=
|
||
if x > 0 then f (x-1) * 2 else 1 -- Error
|
||
|
||
protected partial def Bla.f (x : Nat) :=
|
||
if x > 0 then Bla.f (x-1) * 2 else 1
|
||
|
||
#eval Bla.f 3
|
||
|
||
namespace Foo
|
||
|
||
protected partial def g (x : Nat) :=
|
||
if x > 0 then g (x-1) * 2 else 1 -- error
|
||
|
||
end Foo
|
||
|
||
namespace Bla
|
||
|
||
protected partial def g (x : Nat) :=
|
||
if x > 0 then Bla.g (x-1) * 2 else 1
|
||
|
||
#eval g 3 -- error
|
||
|
||
#eval Bla.g 3
|
||
|
||
end Bla
|
||
|
||
|
||
def S (σ : Type) (m : Type → Type) (α : Type) :=
|
||
σ → m (α × σ)
|
||
|
||
namespace S
|
||
variable {σ : Type} {m : Type → Type} [Monad m] {α : Type}
|
||
|
||
protected def pure (a : α) : S σ m α :=
|
||
fun s => pure (a, s) -- This `pure` is the top-level one. The `pure` being defined here is called `S.pure`.
|
||
|
||
end S
|