From cb06d0a9590ed045b349c7c2851d7b9b1a56ff58 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2013 20:18:48 -0700 Subject: [PATCH] test(frontends/lean): add example showing higher order matching is working, and is useful Signed-off-by: Leonardo de Moura --- tests/lean/ho.lean | 7 +++++++ tests/lean/ho.lean.expected.out | 10 ++++++++++ 2 files changed, 17 insertions(+) create mode 100644 tests/lean/ho.lean create mode 100644 tests/lean/ho.lean.expected.out diff --git a/tests/lean/ho.lean b/tests/lean/ho.lean new file mode 100644 index 000000000..e17e19e57 --- /dev/null +++ b/tests/lean/ho.lean @@ -0,0 +1,7 @@ +Variable g {A : Type} (a : A) : A +Variable a : Int +Variable b : Int +Axiom H1 : a = b +Axiom H2 : (g a) > 0 +Theorem T1 : (g b) > 0 := Subst _ H2 H1 +Show Environment 2 diff --git a/tests/lean/ho.lean.expected.out b/tests/lean/ho.lean.expected.out new file mode 100644 index 000000000..bb69c70ad --- /dev/null +++ b/tests/lean/ho.lean.expected.out @@ -0,0 +1,10 @@ + Set: pp::colors + Set: pp::unicode + Assumed: g + Assumed: a + Assumed: b + Assumed: H1 + Assumed: H2 + Proved: T1 +Axiom H2 : (g a) > 0 +Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, if Bool ((g x) ≤ 0) ⊥ ⊤) H2 H1