From 6f3fa63ccb09d1f87c2db67182beb693300de9ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 14:51:34 -0700 Subject: [PATCH] Add missing test Signed-off-by: Leonardo de Moura --- src/tests/kernel/normalizer.cpp | 3 ++- tests/lean/tst8.lean | 3 +++ tests/lean/tst8.lean.expected.out | 2 ++ 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index e5df2d1f5..05e1ecc77 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -233,7 +233,7 @@ static void tst5() { #endif } -void tst6() { +static void tst6() { environment env; expr x = Const("x"); expr t = Fun({x, Type()}, mk_app(x, x)); @@ -253,5 +253,6 @@ int main() { tst3(); tst4(); tst5(); + tst6(); return has_violations() ? 1 : 0; } diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean index 6aef8a164..7c1baff1e 100644 --- a/tests/lean/tst8.lean +++ b/tests/lean/tst8.lean @@ -8,3 +8,6 @@ Definition f (A: Type) (a : A) : A := let b := g A a, c := g A b in c + +Show f _ 10. +Show f _ (- 10). diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out index 81384291f..09a98f224 100644 --- a/tests/lean/tst8.lean.expected.out +++ b/tests/lean/tst8.lean.expected.out @@ -3,3 +3,5 @@ Π (A : Type) (a : A), A Assumed: g Defined: f +f Nat 10 +f Int (- 10)