test(tests/lean/run): add section test
This commit is contained in:
parent
8c11dc1ecd
commit
5cff53c447
1 changed files with 17 additions and 0 deletions
17
tests/lean/run/section2.lean
Normal file
17
tests/lean/run/section2.lean
Normal file
|
@ -0,0 +1,17 @@
|
||||||
|
import data.nat
|
||||||
|
|
||||||
|
section foo
|
||||||
|
parameter A : Type
|
||||||
|
definition id (a : A) := a
|
||||||
|
variable a : nat
|
||||||
|
check _root_.id nat a
|
||||||
|
end foo
|
||||||
|
|
||||||
|
namespace n1
|
||||||
|
section foo
|
||||||
|
parameter A : Type
|
||||||
|
definition id (a : A) := a
|
||||||
|
variable a : nat
|
||||||
|
check n1.id _ a
|
||||||
|
end foo
|
||||||
|
end n1
|
Loading…
Add table
Reference in a new issue