michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/interactive/findp): adjust test output to reflect recent changes in the pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-08 09:49:22 -07:00
parent eb5089bf27
commit 24f1454c0a
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
tests/lean/interactive/findp.input.expected.out
View file

@ -7,14 +7,15 @@ false.of_ne|?a ≠ ?a → false
false.rec_on|Π (C : Type), false → C false.rec_on|Π (C : Type), false → C
false.cases_on|Π (C : Type), false → C false.cases_on|Π (C : Type), false → C
false.induction_on|∀ (C : Prop), false → C false.induction_on|∀ (C : Prop), false → C
true_ne_false|¬ true = false true_ne_false|¬true = false
not_of_is_false|is_false ?c → ¬ ?c not_of_is_false|is_false ?c → ¬?c
not_of_iff_false|?a ↔ false → ¬ ?a not_of_iff_false|?a ↔ false → ¬?a
p_ne_false|?p → ?p ≠ false p_ne_false|?p → ?p ≠ false
is_false|Π (c : Prop) [H : decidable c], Prop is_false|Π (c : Prop) [H : decidable c], Prop
not_of_eq_false|?p = false → ¬ ?p not_of_eq_false|?p = false → ¬?p
decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2 decidable.rec_on_false|Π (H3 : ¬?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
not_false|¬ false not_false|¬false
decidable_false|decidable false decidable_false|decidable false
of_not_is_false|¬ is_false ?c → ?c of_not_is_false|¬is_false ?c → ?c
iff_false_intro|¬?a → ?a ↔ false
-- ENDFINDP -- ENDFINDP