From 9f4959fb644ba1d79d9af82411472feb81b9b608 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2014 15:19:52 -0800 Subject: [PATCH] test(tests/lean): kernel exception pp method Signed-off-by: Leonardo de Moura --- tests/lean/kernel_ex1.lean | 6 ++++++ tests/lean/kernel_ex1.lean.expected.out | 15 +++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 tests/lean/kernel_ex1.lean create mode 100644 tests/lean/kernel_ex1.lean.expected.out diff --git a/tests/lean/kernel_ex1.lean b/tests/lean/kernel_ex1.lean new file mode 100644 index 000000000..85cb8b023 --- /dev/null +++ b/tests/lean/kernel_ex1.lean @@ -0,0 +1,6 @@ +variable N : Type +variable a : N +check fun x : a, x +check a a +variable f : N -> N +check f (fun x : N, x) \ No newline at end of file diff --git a/tests/lean/kernel_ex1.lean.expected.out b/tests/lean/kernel_ex1.lean.expected.out new file mode 100644 index 000000000..be5da0b38 --- /dev/null +++ b/tests/lean/kernel_ex1.lean.expected.out @@ -0,0 +1,15 @@ + Set: pp::colors + Set: pp::unicode + Assumed: N + Assumed: a +Error (line: 3, pos: 14) type expected, got + a +Error (line: 4, pos: 6) function expected at + a a + Assumed: f +Error (line: 6, pos: 6) type mismatch at application + f (λ x : N, x) +Function type: + N → N +Argument type: + (λ x : N, x) : N → N