From 5f790d82cdd12e2acb487633ff1c2624b72e56ce Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 13 Jan 2017 17:41:00 +0100 Subject: [PATCH] fix(test/lean/run/super_tests): fix try_sup API change --- tests/lean/run/super_tests.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/super_tests.lean b/tests/lean/run/super_tests.lean index 7d0c29fae9..06b1a952d0 100644 --- a/tests/lean/run/super_tests.lean +++ b/tests/lean/run/super_tests.lean @@ -6,15 +6,15 @@ example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a) : true := H ← get_local `H >>= clause.of_classical_proof, Hpa ← get_local `Hpa >>= clause.of_classical_proof, a ← get_local `a, -try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate, +try_sup (λx y, ff) H Hpa 0 0 [0] tt ff ``super.sup_ltr >>= clause.validate, to_expr `(trivial) >>= apply example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a → false) (Hpb : p b → false) : true := by do H ← get_local `H >>= clause.of_classical_proof, Hpa ← get_local `Hpa >>= clause.of_classical_proof, Hpb ← get_local `Hpb >>= clause.of_classical_proof, -try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate, -try_sup (λx y, ff) H Hpb 0 0 [0] ff ``super.sup_rtl >>= clause.validate, +try_sup (λx y, ff) H Hpa 0 0 [0] tt ff ``super.sup_ltr >>= clause.validate, +try_sup (λx y, ff) H Hpb 0 0 [0] ff ff ``super.sup_rtl >>= clause.validate, to_expr `(trivial) >>= apply example (i : Type) (p q : i → Prop) (H : ∀x y, p x → q y → false) : true := by do