From 502d9f47acb277245fc2d32bb6cd1b5cb8c60cce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 16:31:52 -0800 Subject: [PATCH] test(tests/lean): new test full of holes Signed-off-by: Leonardo de Moura --- tests/lean/bad10.lean | 8 ++++++++ tests/lean/bad10.lean.expected.out | 8 ++++++++ 2 files changed, 16 insertions(+) create mode 100644 tests/lean/bad10.lean create mode 100644 tests/lean/bad10.lean.expected.out diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean new file mode 100644 index 000000000..ef57c1376 --- /dev/null +++ b/tests/lean/bad10.lean @@ -0,0 +1,8 @@ +SetOption pp::implicit true. +SetOption pp::colors false. +Variable N : Type. + +Definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ := +SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H. + +Show Environment 1. diff --git a/tests/lean/bad10.lean.expected.out b/tests/lean/bad10.lean.expected.out new file mode 100644 index 000000000..0a75399dd --- /dev/null +++ b/tests/lean/bad10.lean.expected.out @@ -0,0 +1,8 @@ + Set: pp::colors + Set: pp::unicode + Set: lean::pp::implicit + Set: pp::colors + Assumed: N + Defined: T +Definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) := + @SubstP N (f a) a (λ x : N, f (f a) == f (f a)) (@Refl N (f (f a))) H