From a34164333514619bc602929026a78bc1a0696f1c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 10:44:51 -0700 Subject: [PATCH] Fix unit tests for Windows Signed-off-by: Leonardo de Moura --- src/tests/frontends/lean/lean_pp.cpp | 5 ++++- tests/lean/arith1.lean | 1 - tests/lean/arith1.lean.expected.out | 1 + tests/lean/arith2.lean.expected.out | 2 ++ tests/lean/arith3.lean | 1 - tests/lean/arith3.lean.expected.out | 1 + tests/lean/arith4.lean.expected.out | 2 ++ tests/lean/arith5.lean.expected.out | 2 ++ tests/lean/coercion1.lean | 1 - tests/lean/coercion1.lean.expected.out | 9 +++++---- tests/lean/coercion2.lean | 1 - tests/lean/coercion2.lean.expected.out | 1 + tests/lean/config.lean | 3 +++ tests/lean/config.lean.expected.out | 4 ++++ tests/lean/deep.lean.expected.out | 4 +++- tests/lean/ex1.lean.expected.out | 2 ++ tests/lean/ex2.lean | 1 - tests/lean/ex2.lean.expected.out | 11 ++++++----- tests/lean/ex3.lean | 1 - tests/lean/ex3.lean.expected.out | 5 +++-- tests/lean/overload1.lean.expected.out | 2 ++ tests/lean/overload2.lean | 1 - tests/lean/overload2.lean.expected.out | 5 +++-- tests/lean/test.sh | 2 +- tests/lean/tst1.lean | 1 - tests/lean/tst1.lean.expected.out | 1 + tests/lean/tst10.lean | 1 - tests/lean/tst10.lean.expected.out | 1 + tests/lean/tst11.lean | 1 - tests/lean/tst11.lean.expected.out | 1 + tests/lean/tst12.lean | 1 - tests/lean/tst12.lean.expected.out | 1 + tests/lean/tst13.lean | 1 - tests/lean/tst13.lean.expected.out | 1 + tests/lean/tst14.lean | 1 - tests/lean/tst14.lean.expected.out | 1 + tests/lean/tst15.lean | 1 - tests/lean/tst15.lean.expected.out | 1 + tests/lean/tst16.lean | 1 - tests/lean/tst16.lean.expected.out | 1 + tests/lean/tst17.lean | 1 - tests/lean/tst17.lean.expected.out | 1 + tests/lean/tst2.lean.expected.out | 12 +++++++----- tests/lean/tst3.lean | 1 - tests/lean/tst3.lean.expected.out | 1 + tests/lean/tst4.lean | 1 - tests/lean/tst4.lean.expected.out | 5 +++-- tests/lean/tst5.lean | 1 - tests/lean/tst5.lean.expected.out | 1 + tests/lean/tst6.lean | 1 - tests/lean/tst6.lean.expected.out | 1 + tests/lean/tst7.lean | 1 - tests/lean/tst7.lean.expected.out | 3 ++- tests/lean/tst8.lean | 1 - tests/lean/tst8.lean.expected.out | 1 + tests/lean/tst9.lean | 1 - tests/lean/tst9.lean.expected.out | 3 ++- tests/lean/unicode.lean | 1 - tests/lean/unicode.lean.expected.out | 1 + 59 files changed, 73 insertions(+), 49 deletions(-) create mode 100644 tests/lean/config.lean create mode 100644 tests/lean/config.lean.expected.out diff --git a/src/tests/frontends/lean/lean_pp.cpp b/src/tests/frontends/lean/lean_pp.cpp index eceaae8cf..12b0baf14 100644 --- a/src/tests/frontends/lean/lean_pp.cpp +++ b/src/tests/frontends/lean/lean_pp.cpp @@ -74,6 +74,8 @@ static void tst5() { frontend f; std::shared_ptr out(new string_output_channel()); f.set_regular_channel(out); + f.set_option(name{"pp", "unicode"}, true); + f.set_option(name{"lean", "pp", "notation"}, true); regular(f) << And(Const("a"), Const("b")); lean_assert(out->str() == "a ∧ b"); f.set_option(name{"lean", "pp", "notation"}, false); @@ -95,8 +97,9 @@ static void tst6() { expr t = mk_deep(10); f.set_option(name{"lean", "pp", "max_depth"}, 5); f.set_option(name{"pp", "colors"}, false); + f.set_option(name{"pp", "unicode"}, false); regular(f) << t; - lean_assert(out->str() == "f (f (f (f (f (…)))))"); + lean_assert(out->str() == "f (f (f (f (f (...)))))"); } int main() { diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean index 3d2042dab..c6d69929c 100644 --- a/tests/lean/arith1.lean +++ b/tests/lean/arith1.lean @@ -1,4 +1,3 @@ -Set pp::colors false Check 10 + 20 Check 10 Check 10 - 20 diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out index c7879fe83..d2113d250 100644 --- a/tests/lean/arith1.lean.expected.out +++ b/tests/lean/arith1.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Nat Nat Int diff --git a/tests/lean/arith2.lean.expected.out b/tests/lean/arith2.lean.expected.out index 9b53ea364..4dc874481 100644 --- a/tests/lean/arith2.lean.expected.out +++ b/tests/lean/arith2.lean.expected.out @@ -1,3 +1,5 @@ + Set: pp::colors + Set: pp::unicode 1 / 2 2/3 3 div 2 diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean index 015976101..25b4427a3 100644 --- a/tests/lean/arith3.lean +++ b/tests/lean/arith3.lean @@ -1,4 +1,3 @@ -Set pp::colors false Eval 8 mod 3 Eval 8 div 4 Eval 7 div 3 diff --git a/tests/lean/arith3.lean.expected.out b/tests/lean/arith3.lean.expected.out index c581c4c75..9958e2234 100644 --- a/tests/lean/arith3.lean.expected.out +++ b/tests/lean/arith3.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode 2 2 2 diff --git a/tests/lean/arith4.lean.expected.out b/tests/lean/arith4.lean.expected.out index 3d819ea0b..52a026614 100644 --- a/tests/lean/arith4.lean.expected.out +++ b/tests/lean/arith4.lean.expected.out @@ -1,3 +1,5 @@ + Set: pp::colors + Set: pp::unicode Assumed: x sin x sin (x + -1 * (π / 2)) diff --git a/tests/lean/arith5.lean.expected.out b/tests/lean/arith5.lean.expected.out index 703a32289..06097b9f1 100644 --- a/tests/lean/arith5.lean.expected.out +++ b/tests/lean/arith5.lean.expected.out @@ -1,3 +1,5 @@ + Set: pp::colors + Set: pp::unicode Assumed: x (1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x))) (1 + (exp (-2 * x))) / (2 * (exp (-1 * x))) diff --git a/tests/lean/coercion1.lean b/tests/lean/coercion1.lean index 980b7f13a..7a0002dbb 100644 --- a/tests/lean/coercion1.lean +++ b/tests/lean/coercion1.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable T : Type Variable R : Type Variable f : T -> R diff --git a/tests/lean/coercion1.lean.expected.out b/tests/lean/coercion1.lean.expected.out index dcd88cca1..1a686fa4d 100644 --- a/tests/lean/coercion1.lean.expected.out +++ b/tests/lean/coercion1.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: T Assumed: R Assumed: f @@ -6,12 +7,12 @@ Variable f : T → R Coercion f Assumed: g -Error (line: 9, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types +Error (line: 8, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types Assumed: h -Error (line: 11, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) +Error (line: 10, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type) Defined: T2 Defined: R2 Assumed: f2 -Error (line: 15, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types +Error (line: 14, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types Assumed: id -Error (line: 17, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same +Error (line: 16, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same diff --git a/tests/lean/coercion2.lean b/tests/lean/coercion2.lean index f6725e50b..12253dad7 100644 --- a/tests/lean/coercion2.lean +++ b/tests/lean/coercion2.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable T : Type Variable R : Type Variable t2r : T -> R diff --git a/tests/lean/coercion2.lean.expected.out b/tests/lean/coercion2.lean.expected.out index 2ef6f55f3..9e0b4241f 100644 --- a/tests/lean/coercion2.lean.expected.out +++ b/tests/lean/coercion2.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: T Assumed: R Assumed: t2r diff --git a/tests/lean/config.lean b/tests/lean/config.lean new file mode 100644 index 000000000..905e75340 --- /dev/null +++ b/tests/lean/config.lean @@ -0,0 +1,3 @@ +(* Set default configuration for tests *) +Set pp::colors false +Set pp::unicode true diff --git a/tests/lean/config.lean.expected.out b/tests/lean/config.lean.expected.out new file mode 100644 index 000000000..7e317fecc --- /dev/null +++ b/tests/lean/config.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode + Set: pp::colors + Set: pp::unicode diff --git a/tests/lean/deep.lean.expected.out b/tests/lean/deep.lean.expected.out index abaf458e7..f9b681097 100644 --- a/tests/lean/deep.lean.expected.out +++ b/tests/lean/deep.lean.expected.out @@ -1,7 +1,9 @@ + Set: pp::colors + Set: pp::unicode Defined: f1 Defined: f2 Defined: f3 Assumed: f Set: pp::width Set: lean::pp::max_depth -f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (…)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (…)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/tests/lean/ex1.lean.expected.out b/tests/lean/ex1.lean.expected.out index 9daeafb98..b6294aaa4 100644 --- a/tests/lean/ex1.lean.expected.out +++ b/tests/lean/ex1.lean.expected.out @@ -1 +1,3 @@ + Set: pp::colors + Set: pp::unicode test diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean index 7651075b6..aba386fa7 100644 --- a/tests/lean/ex2.lean +++ b/tests/lean/ex2.lean @@ -1,6 +1,5 @@ (* comment *) (* (* nested comment *) *) -Set pp::colors false Show true Set lean::pp::notation false Show true && false diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index b49c8fd43..8f9623492 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -1,15 +1,16 @@ Set: pp::colors + Set: pp::unicode ⊤ Set: lean::pp::notation and ⊤ ⊥ Set: pp::unicode and true false Assumed: a -Error (line: 10, pos: 0) invalid object declaration, environment already has an object named 'a' +Error (line: 9, pos: 0) invalid object declaration, environment already has an object named 'a' Assumed: b and a b Assumed: A -Error (line: 14, pos: 11) type mismatch at application +Error (line: 13, pos: 11) type mismatch at application and a A Function type: Bool -> Bool -> Bool @@ -17,8 +18,8 @@ Arguments types: Bool Type Variable A : Type -(pp::unicode := false, lean::pp::notation := false, pp::colors := false) -Error (line: 17, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options -Error (line: 18, pos: 23) invalid option value, given option is not an integer +(lean::pp::notation := false, pp::unicode := false, pp::colors := false) +Error (line: 16, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options +Error (line: 17, pos: 23) invalid option value, given option is not an integer Set: lean::pp::notation a /\ b diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean index b5949784b..9154da3c8 100644 --- a/tests/lean/ex3.lean +++ b/tests/lean/ex3.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable myeq : Pi (A : Type), A -> A -> Bool Show myeq _ true false Variable T : Type diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out index 881c4026b..496d4e1a1 100644 --- a/tests/lean/ex3.lean.expected.out +++ b/tests/lean/ex3.lean.expected.out @@ -1,9 +1,10 @@ Set: pp::colors + Set: pp::unicode Assumed: myeq myeq Bool ⊤ ⊥ Assumed: T Assumed: a -Error (line: 6, pos: 6) type mismatch at application +Error (line: 5, pos: 6) type mismatch at application myeq Bool ⊤ a Function type: Π (A : Type) (_ _ : A), Bool @@ -13,7 +14,7 @@ Arguments types: T Assumed: myeq2 Set: lean::pp::implicit -Error (line: 10, pos: 15) type mismatch at application +Error (line: 9, pos: 15) type mismatch at application myeq2::explicit Bool ⊤ a Function type: Π (A : Type) (a b : A), Bool diff --git a/tests/lean/overload1.lean.expected.out b/tests/lean/overload1.lean.expected.out index d06cf117b..113d03bbf 100644 --- a/tests/lean/overload1.lean.expected.out +++ b/tests/lean/overload1.lean.expected.out @@ -1,3 +1,5 @@ + Set: pp::colors + Set: pp::unicode Assumed: N Assumed: f Assumed: g diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean index f75cf84e8..6c238c5d7 100644 --- a/tests/lean/overload2.lean +++ b/tests/lean/overload2.lean @@ -1,4 +1,3 @@ -Set pp::colors false Show 1 + true Variable R : Type Variable T : Type diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index 41b0ea603..1d481a8d9 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors -Error (line: 2, pos: 9) application type mismatch, none of the overloads can be used + Set: pp::unicode +Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used Candidates: Real::add : Real → Real → Real Int::add : Int → Int → Int @@ -22,7 +23,7 @@ f a b f (r2t b) (t2r a) Assumed: g f a b -Error (line: 20, pos: 10) ambiguous overloads +Error (line: 19, pos: 10) ambiguous overloads Candidates: g : R → T → R f : T → R → T diff --git a/tests/lean/test.sh b/tests/lean/test.sh index 21a4b5b75..e89475da3 100755 --- a/tests/lean/test.sh +++ b/tests/lean/test.sh @@ -13,7 +13,7 @@ fi NUM_ERRORS=0 for f in `ls *.lean`; do echo "-- testing $f" - $LEAN $f > $f.produced.out + $LEAN config.lean $f > $f.produced.out if test -f $f.expected.out; then if diff $f.produced.out $f.expected.out; then echo "-- checked" diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean index 4e8ed0173..28a8455e5 100644 --- a/tests/lean/tst1.lean +++ b/tests/lean/tst1.lean @@ -1,4 +1,3 @@ -Set pp::colors false (* Define a "fake" type to simulate the natural numbers. This is just a test. *) Variable N : Type Variable lt : N -> N -> Bool diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index f647e85ed..cddeeb831 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: N Assumed: lt Assumed: zero diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean index a1454951a..d3413e0fb 100644 --- a/tests/lean/tst10.lean +++ b/tests/lean/tst10.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable a : Bool Variable b : Bool (* Conjunctions *) diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out index 5ad512be1..9fd43784a 100644 --- a/tests/lean/tst10.lean.expected.out +++ b/tests/lean/tst10.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: a Assumed: b a ∧ b diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean index 9a4c99a32..a34f54bd3 100644 --- a/tests/lean/tst11.lean +++ b/tests/lean/tst11.lean @@ -1,4 +1,3 @@ -Set pp::colors false Definition xor (x y : Bool) : Bool := (not x) = y Infixr 50 ⊕ : xor Show xor true false diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out index 9bd8300b5..b71e8b076 100644 --- a/tests/lean/tst11.lean.expected.out +++ b/tests/lean/tst11.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Defined: xor ⊤ ⊕ ⊥ ⊥ diff --git a/tests/lean/tst12.lean b/tests/lean/tst12.lean index a163972c2..74ff3a4b9 100644 --- a/tests/lean/tst12.lean +++ b/tests/lean/tst12.lean @@ -1,4 +1,3 @@ -Set pp::colors false Show (fun x : Bool, (fun y : Bool, x /\ y)) Show let x := true, y := true diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out index 44366bbaa..bfa3d8597 100644 --- a/tests/lean/tst12.lean.expected.out +++ b/tests/lean/tst12.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode λ x y : Bool, x ∧ y let x := ⊤, y := ⊤, diff --git a/tests/lean/tst13.lean b/tests/lean/tst13.lean index 0536677cf..6841ab845 100644 --- a/tests/lean/tst13.lean +++ b/tests/lean/tst13.lean @@ -1,4 +1,3 @@ -Set pp::colors false Show fun x : Bool, (fun x : Bool, x). Show let x := true, y := true diff --git a/tests/lean/tst13.lean.expected.out b/tests/lean/tst13.lean.expected.out index fa6041aea..433c9bb11 100644 --- a/tests/lean/tst13.lean.expected.out +++ b/tests/lean/tst13.lean.expected.out @@ -1,3 +1,4 @@ Set: pp::colors + Set: pp::unicode λ x x : Bool, x let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z diff --git a/tests/lean/tst14.lean b/tests/lean/tst14.lean index 262e5f5e9..bc5ab03e2 100644 --- a/tests/lean/tst14.lean +++ b/tests/lean/tst14.lean @@ -1,4 +1,3 @@ -Set pp::colors false Show Int -> Int -> Int Variable f : Int -> Int -> Int Eval f 0 diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out index a7179fc1e..0c0344298 100644 --- a/tests/lean/tst14.lean.expected.out +++ b/tests/lean/tst14.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Int → Int → Int Assumed: f f 0 diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean index 78ff5ce3c..1b2fedc44 100644 --- a/tests/lean/tst15.lean +++ b/tests/lean/tst15.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable x : Type max U+1+2 M+1 M+2 3 Check x Variable f : Type U+10 -> Type diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out index 70c49b085..007e513d4 100644 --- a/tests/lean/tst15.lean.expected.out +++ b/tests/lean/tst15.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: x Type U+3 ⊔ M+2 ⊔ 3 Assumed: f diff --git a/tests/lean/tst16.lean b/tests/lean/tst16.lean index 90768808f..ce0732e90 100644 --- a/tests/lean/tst16.lean +++ b/tests/lean/tst16.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable f : Type -> Bool Show forall a b : Type, (f a) = (f b) Variable g : Bool -> Bool -> Bool diff --git a/tests/lean/tst16.lean.expected.out b/tests/lean/tst16.lean.expected.out index e72882484..f0852e2fa 100644 --- a/tests/lean/tst16.lean.expected.out +++ b/tests/lean/tst16.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: f ∀ a b : Type, (f a) = (f b) Assumed: g diff --git a/tests/lean/tst17.lean b/tests/lean/tst17.lean index 95083cfab..c335b8f2e 100644 --- a/tests/lean/tst17.lean +++ b/tests/lean/tst17.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable f : Type -> Bool Variable g : Type -> Type -> Bool Show forall (a b : Type), exists (c : Type), (g a b) = (f c) diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out index 9989c3d24..001782e7f 100644 --- a/tests/lean/tst17.lean.expected.out +++ b/tests/lean/tst17.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: f Assumed: g ∀ a b : Type, ∃ c : Type, (g a b) = (f c) diff --git a/tests/lean/tst2.lean.expected.out b/tests/lean/tst2.lean.expected.out index 7878b43da..e685a1b71 100644 --- a/tests/lean/tst2.lean.expected.out +++ b/tests/lean/tst2.lean.expected.out @@ -1,12 +1,14 @@ -⟨⟩ + Set: pp::colors + Set: pp::unicode +⟨pp::unicode ↦ true, pp::colors ↦ false⟩ Assumed: a Assumed: b a ∧ b Set: lean::pp::notation -⟨lean::pp::notation ↦ false⟩ +⟨lean::pp::notation ↦ false, pp::unicode ↦ true, pp::colors ↦ false⟩ and a b -Variable a : Bool -Variable b : Bool +Variable a : Bool +Variable b : Bool Set: lean::pp::notation -⟨lean::pp::notation ↦ true⟩ +⟨lean::pp::notation ↦ true, pp::unicode ↦ true, pp::colors ↦ false⟩ a ∧ b diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index 9473c02d9..d370e19cf 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,4 +1,3 @@ -Set pp::colors false Set lean::parser::verbose false. Notation 10 if _ then _ : implies. Show Environment 1. diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out index 68ec51d4d..ce2dec489 100644 --- a/tests/lean/tst3.lean.expected.out +++ b/tests/lean/tst3.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Notation 10 if _ then _ : implies if ⊤ then ⊥ if ⊤ then (if a then ⊥) diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean index 0bd1fc821..aa5236d00 100644 --- a/tests/lean/tst4.lean +++ b/tests/lean/tst4.lean @@ -7,7 +7,6 @@ Show f n1 n2 Show f (fun x : N -> N, x) (fun y : _, y) Variable EqNice {A : Type} (lhs rhs : A) : Bool Infix 50 === : EqNice -Set pp::colors false Show n1 === n2 Check f n1 n2 Check Congr::explicit diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out index 6129bf8f2..dafb8462f 100644 --- a/tests/lean/tst4.lean.expected.out +++ b/tests/lean/tst4.lean.expected.out @@ -1,12 +1,13 @@ + Set: pp::colors + Set: pp::unicode Assumed: f Assumed: N Assumed: n1 Assumed: n2 Set: lean::pp::implicit f::explicit N n1 n2 -f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y) +f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y) Assumed: EqNice - Set: pp::colors EqNice::explicit N n1 n2 N Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b) diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean index 1f0297d6a..11444d46c 100644 --- a/tests/lean/tst5.lean +++ b/tests/lean/tst5.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable N : Type Variable a : N Variable b : N diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out index 23bb86f6f..8d44df450 100644 --- a/tests/lean/tst5.lean.expected.out +++ b/tests/lean/tst5.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: N Assumed: a Assumed: b diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean index e63041696..e13f1eab9 100644 --- a/tests/lean/tst6.lean +++ b/tests/lean/tst6.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable N : Type Variable h : N -> N -> N diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 8dc00e7e4..905264392 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Assumed: N Assumed: h Proved: CongrH diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean index f4fdde023..ca3cd1d30 100644 --- a/tests/lean/tst7.lean +++ b/tests/lean/tst7.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable f : Pi (A : Type), A -> Bool Show fun (A B : Type) (a : _), f B a (* The following one should produce an error *) diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out index c3a3d7f86..74a88fbea 100644 --- a/tests/lean/tst7.lean.expected.out +++ b/tests/lean/tst7.lean.expected.out @@ -1,7 +1,8 @@ Set: pp::colors + Set: pp::unicode Assumed: f λ (A B : Type) (a : B), f B a -Error (line: 5, pos: 40) application type mismatch during term elaboration at term +Error (line: 4, pos: 40) application type mismatch during term elaboration at term f B a Elaborator state #0 ≈ lift:0:2 ?M0 diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean index c047e451a..6aef8a164 100644 --- a/tests/lean/tst8.lean +++ b/tests/lean/tst8.lean @@ -1,4 +1,3 @@ -Set pp::colors false Check fun (A : Type) (a : A), let b := a in b diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out index 97e3f6559..81384291f 100644 --- a/tests/lean/tst8.lean.expected.out +++ b/tests/lean/tst8.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode Π (A : Type) (a : A), A Assumed: g Defined: f diff --git a/tests/lean/tst9.lean b/tests/lean/tst9.lean index ab5917102..89f5efc9b 100644 --- a/tests/lean/tst9.lean +++ b/tests/lean/tst9.lean @@ -1,4 +1,3 @@ -Set pp::colors false Variable f : Pi A : Type, A -> A -> A Variable N : Type Variable g : N -> N -> Bool diff --git a/tests/lean/tst9.lean.expected.out b/tests/lean/tst9.lean.expected.out index d77e1c8ed..60840f342 100644 --- a/tests/lean/tst9.lean.expected.out +++ b/tests/lean/tst9.lean.expected.out @@ -1,9 +1,10 @@ Set: pp::colors + Set: pp::unicode Assumed: f Assumed: N Assumed: g Assumed: a -Error (line: 6, pos: 6) type mismatch at application +Error (line: 5, pos: 6) type mismatch at application g ⊤ (f _ a a) Function type: N → N → Bool diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean index c24432cf2..356b0a6b8 100644 --- a/tests/lean/unicode.lean +++ b/tests/lean/unicode.lean @@ -1,4 +1,3 @@ -Set pp::colors false Show true /\ false Set pp::unicode false Show true /\ false diff --git a/tests/lean/unicode.lean.expected.out b/tests/lean/unicode.lean.expected.out index a0da64bc2..0d91b2969 100644 --- a/tests/lean/unicode.lean.expected.out +++ b/tests/lean/unicode.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors + Set: pp::unicode ⊤ ∧ ⊥ Set: pp::unicode true /\ false