From 390f7eaec88326af603fdcab93edca1894695ddc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Nov 2013 15:01:39 -0800 Subject: [PATCH] test(kernel/typechecker): type checker Signed-off-by: Leonardo de Moura --- tests/lean/ty2.lean | 6 ++++++ tests/lean/ty2.lean.expected.out | 8 ++++++++ 2 files changed, 14 insertions(+) create mode 100644 tests/lean/ty2.lean create mode 100644 tests/lean/ty2.lean.expected.out diff --git a/tests/lean/ty2.lean b/tests/lean/ty2.lean new file mode 100644 index 000000000..f07cbfc64 --- /dev/null +++ b/tests/lean/ty2.lean @@ -0,0 +1,6 @@ +Definition B : Type := Bool +Definition T : Type 1 := Type +Variable N : T +Variable x : N +Variable a : B +Axiom H : a diff --git a/tests/lean/ty2.lean.expected.out b/tests/lean/ty2.lean.expected.out new file mode 100644 index 000000000..53dc668cd --- /dev/null +++ b/tests/lean/ty2.lean.expected.out @@ -0,0 +1,8 @@ + Set: pp::colors + Set: pp::unicode + Defined: B + Defined: T + Assumed: N + Assumed: x + Assumed: a + Assumed: H