Mathlib v3 is deprecated. Go to Mathlib v4

Def mk_iff.list_option_merge

Modification history

2020-11-03 17:56
src/tactic/mk_iff_of_inductive_prop.lean
feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863) …
Added mk_iff.list_option_mergeView on Github →