Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-03 17:56 4f8c490f

View on Github →

feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863) This attribute should make mk_iff_of_inductive_prop easier to use.

Estimated changes

modified structure problem_predicate
modified inductive multiset.rel
modified inductive perfect_closure.r
modified inductive relation.refl_gen
modified inductive relation.trans_gen
added structure foo2
added structure foo