From 6d9a342f1761c64fc5ab55857efaba6fa848ebd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Aug 2013 22:14:27 -0700 Subject: [PATCH] Add regression test to expose bug fixed in previous commit. Signed-off-by: Leonardo de Moura --- src/tests/kernel/free_vars.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index f5e741ecff..89f531108a 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "free_vars.h" +#include "abstract.h" #include "test.h" using namespace lean; @@ -29,8 +30,19 @@ static void tst1() { lean_assert(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1) == mk_lambda("_", t, f(Var(0)))); } +static void tst2() { + expr f = Const("f"); + expr x = Const("x"); + expr y = Const("y"); + expr B = Const("Bool"); + expr t = Fun({x, B}, Fun({y, B}, x)); + lean_assert(closed(t)); + lean_assert(!closed(abst_body(t))); +} + int main() { continue_on_violation(true); tst1(); + tst2(); return has_violations() ? 1 : 0; }