Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-04 16:10 e4c64fd9

View on Github →

feat(tactic/mk_iff_of_inductive_prop): add tactic to represent inductives using logical connectives

Estimated changes

Modified data/list/basic.lean

Modified logic/relation.lean

modified theorem relation.refl_gen.to_refl_trans_gen

modified theorem relation.refl_trans_gen.cases_tail

deleted theorem relation.refl_trans_gen.cases_tail_iff

Modified tactic/default.lean

Created tactic/mk_iff_of_inductive_prop.lean

Created tests/mk_iff_of_inductive.lean

added inductive multiset.rel

added inductive test.is_true