From a37e24af4acfae019f716ac4faec9a4e753b7e48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Nov 2020 15:39:22 -0800 Subject: [PATCH] test: `_root_` cc @Kha --- tests/lean/run/root.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lean/run/root.lean diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean new file mode 100644 index 0000000000..9eacc12c4b --- /dev/null +++ b/tests/lean/run/root.lean @@ -0,0 +1,17 @@ +def x := 10 + + +namespace Foo + +def x := true + +#check x +#check _root_.x + +theorem ex1 : x = true := rfl +theorem ex2 : _root_.x = 10 := rfl + +end Foo + +theorem ex3 : x = 10 := rfl +theorem ex4 : _root_.x = 10 := rfl