lean2/tests/lean/interactive/findp.input.expected.out

-- BEGINWAIT
-- ENDWAIT
-- BEGINFINDP STALE
false|Prop
false.rec|Π (C : Type), false → C
false.of_ne|?a ≠ ?a → false
false.rec_on|Π (C : Type), false → C
false.cases_on|Π (C : Type), false → C
false.decidable|decidable false
false.induction_on|∀ (C : Prop), false → C
true_ne_false|¬ true = false
not_of_is_false|is_false ?c → ¬ ?c
not_of_iff_false|?a ↔ false → ¬ ?a
p_ne_false|?p → ?p ≠ false
is_false|Π (c : Prop) [H : decidable c], Prop
not_of_eq_false|?p = false → ¬ ?p
decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
not_false|¬ false
of_not_is_false|¬ is_false ?c → ?c
-- ENDFINDP
feat(frontends/lean/server): sort exact matches by size in FINDP 2014-09-29 16:40:17 -07:00			`-- BEGINWAIT`
			`-- ENDWAIT`
			`-- BEGINFINDP STALE`
			`false\|Prop`
fix(kernel/inductive): relax eliminator generation rules for empty types This commit also removes the workaround false.rec_type. It is not needed anymore 2014-10-28 10:31:00 -07:00			`false.rec\|Π (C : Type), false → C`
fix(tests/lean): adjust tests to modifications to standard library 2014-11-30 21:16:01 -08:00			`false.of_ne\|?a ≠ ?a → false`
fix(kernel/inductive): relax eliminator generation rules for empty types This commit also removes the workaround false.rec_type. It is not needed anymore 2014-10-28 10:31:00 -07:00			`false.rec_on\|Π (C : Type), false → C`
feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00			`false.cases_on\|Π (C : Type), false → C`
fix(tests/lean): adjust tests to modifications to standard library 2014-11-30 21:16:01 -08:00			`false.decidable\|decidable false`
feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:36:38 -07:00			`false.induction_on\|∀ (C : Prop), false → C`
feat(frontends/lean/pp): take notation declarations into account when pretty printing TODO: support foldl/foldr and binders 2014-10-19 08:40:56 -07:00			`true_ne_false\|¬ true = false`
fix(tests/lean/interactive): adjust test to reflect changes in the standard library 2014-12-11 19:53:41 -08:00			`not_of_is_false\|is_false ?c → ¬ ?c`
refactor(library/init): move more theorems to logic 2014-12-12 13:50:53 -08:00			`not_of_iff_false\|?a ↔ false → ¬ ?a`
feat(frontends/lean/pp): take notation declarations into account when pretty printing TODO: support foldl/foldr and binders 2014-10-19 08:40:56 -07:00			`p_ne_false\|?p → ?p ≠ false`
fix(tests/lean/interactive): adjust test to reflect changes in the standard library 2014-12-11 19:53:41 -08:00			`is_false\|Π (c : Prop) [H : decidable c], Prop`
refactor(library/init): move more theorems to logic 2014-12-12 13:50:53 -08:00			`not_of_eq_false\|?p = false → ¬ ?p`
fix(tests/lean): adjust tests to modifications to standard library 2014-11-30 21:16:01 -08:00			`decidable.rec_on_false\|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2`
			`not_false\|¬ false`
fix(tests/lean/interactive): adjust test to reflect changes in the standard library 2014-12-11 19:53:41 -08:00			`of_not_is_false\|¬ is_false ?c → ?c`
feat(frontends/lean/server): sort exact matches by size in FINDP 2014-09-29 16:40:17 -07:00			`-- ENDFINDP`