From 5cff53c447a8c5ef084df6156594ef910fbc6731 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Sep 2014 15:32:50 -0700 Subject: [PATCH] test(tests/lean/run): add section test --- tests/lean/run/section2.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lean/run/section2.lean diff --git a/tests/lean/run/section2.lean b/tests/lean/run/section2.lean new file mode 100644 index 000000000..3a637d538 --- /dev/null +++ b/tests/lean/run/section2.lean @@ -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