From 5a38e15c2e4498fbacb07a416dd4e19c182167ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 6 Aug 2016 14:18:08 -0700 Subject: [PATCH] test(tests/lean/run/match_expr2): match example with abstract structures --- tests/lean/run/match_expr2.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/lean/run/match_expr2.lean diff --git a/tests/lean/run/match_expr2.lean b/tests/lean/run/match_expr2.lean new file mode 100644 index 0000000000..a9f72e7901 --- /dev/null +++ b/tests/lean/run/match_expr2.lean @@ -0,0 +1,13 @@ +import algebra.ordered_ring +open tactic +axiom Sorry : ∀ {A:Type}, A + +example {A : Type} [ordered_ring A] (a b c : A) (h₀ : c > 0) (h₁ : a > 1) (h₂ : b > 0) : a + b + c = 0 := +by do + [x, y] ← match_target_subexpr `(λ x y : A, x + y) | failed, + trace "------ subterms -------", + trace x, trace y, + (h, [z]) ← match_hypothesis `(λ x : A, x > 1) | failed, + trace "--- hypothesis of the form x > 1 ---", + trace h, trace z, + refine `(Sorry)