From a35fd06a339809aa47f99791bdb46ecd9b095e90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Dec 2015 10:21:10 -0800 Subject: [PATCH] test(tests/lean/run/blast_simp4): add simp test --- tests/lean/run/blast_simp4.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/lean/run/blast_simp4.lean diff --git a/tests/lean/run/blast_simp4.lean b/tests/lean/run/blast_simp4.lean new file mode 100644 index 0000000000..0b5d5e89c1 --- /dev/null +++ b/tests/lean/run/blast_simp4.lean @@ -0,0 +1,15 @@ +import data.nat +open nat + +constant f : nat → nat +definition g (a : nat) := a + + +example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) := +suppose a + 0 = 0 + g b, +assert a = b, by unfold g at *; simp, +by simp + +attribute g [reducible] +example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) := +by simp