From b9d7f8e8675ff93b8b1eebdb8404da998eec9ecd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 May 2014 13:34:04 -0700 Subject: [PATCH] test(lua): make sure bug reported by Floris does not happen in Lean 0.2 Signed-off-by: Leonardo de Moura --- tests/lua/level9.lua | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/lua/level9.lua diff --git a/tests/lua/level9.lua b/tests/lua/level9.lua new file mode 100644 index 0000000000..ee145f441f --- /dev/null +++ b/tests/lua/level9.lua @@ -0,0 +1,4 @@ +local l = param_univ("l") +assert(l+0 == l) +local l = mk_level_zero() +assert(l+0 == mk_level_zero())