max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(test/lean/run/super_tests): fix try_sup API change

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-13 17:41:00 +01:00 • committed by Leonardo de Moura
parent 6f8fc0fe06
commit 5f790d82cd
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/super_tests.lean
View file

@ -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