Commit 2022-11-14 10:01 35aa345c

View on Github →

refactor: docs and simplifications for mk_iff (#595) Some cleanup and documentation for #561.

Estimated changes

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

added structure Mathlib.Tactic.MkIff.Shape

added def Mathlib.Tactic.MkIff.listBoolMerge

deleted def Mathlib.Tactic.MkIff.listOptionMerge

modified def Mathlib.Tactic.MkIff.toCases

Modified test/MkIffOfInductive.lean