From daadff548e0196f5e3f9712f2062f78ae66f2871 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Dec 2013 16:31:13 -0800 Subject: [PATCH] fix(tests/lean): update expected result to reflect recent changes Signed-off-by: Leonardo de Moura --- tests/lean/tactic2.lean.expected.out | 7 +------ tests/lean/tactic3.lean.expected.out | 7 +------ 2 files changed, 2 insertions(+), 12 deletions(-) diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out index 231a213bb..ce21a1141 100644 --- a/tests/lean/tactic2.lean.expected.out +++ b/tests/lean/tactic2.lean.expected.out @@ -10,9 +10,4 @@ Theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H:: Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p := Discharge (λ H : p, - Discharge - (λ H::1 : p ∧ q, - Discharge - (λ H::2 : r, - Conj (let H::1::2 := Conjunct2 H::1 in H::1::2) - (Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1))))) + Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1))))) diff --git a/tests/lean/tactic3.lean.expected.out b/tests/lean/tactic3.lean.expected.out index 0c84eca2a..8536b12cd 100644 --- a/tests/lean/tactic3.lean.expected.out +++ b/tests/lean/tactic3.lean.expected.out @@ -7,9 +7,4 @@ Theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p := Discharge (λ H : p, - Discharge - (λ H::1 : p ∧ q, - Discharge - (λ H::2 : r, - Conj (let H::1::2 := Conjunct2 H::1 in H::1::2) - (Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1))))) + Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))