michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add missing test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-03 14:51:34 -07:00
parent a154f4e439
commit 6f3fa63ccb
3 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/kernel/normalizer.cpp
View file

@ -233,7 +233,7 @@ static void tst5() {
#endif #endif
} }
void tst6() { static void tst6() {
environment env; environment env;
expr x = Const("x"); expr x = Const("x");
expr t = Fun({x, Type()}, mk_app(x, x)); expr t = Fun({x, Type()}, mk_app(x, x));
@ -253,5 +253,6 @@ int main() {
tst3(); tst3();
tst4(); tst4();
tst5(); tst5();
tst6();
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }

3
tests/lean/tst8.lean
View file

@ -8,3 +8,6 @@ Definition f (A: Type) (a : A) : A :=
let b := g A a, let b := g A a,
c := g A b c := g A b
in c in c
Show f _ 10.
Show f _ (- 10).

2
tests/lean/tst8.lean.expected.out
View file

@ -3,3 +3,5 @@
Π (A : Type) (a : A), A Π (A : Type) (a : A), A
Assumed: g Assumed: g
Defined: f Defined: f
f Nat 10
f Int (- 10)