mathlib
4f8c490f - feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863)

Commit

5 years ago

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

References

Author

bryangingechen

Parents