Commit 2022-11-13 23:24 9de2b435

View on Github →

feat: port mk_iff and mk_iff_of_inductive_prop (#561) This is a direct translation of the mathlib3 version and its tests

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Meta.lean

added def Lean.MVarId.existsi

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/MkIffOfInductiveProp.lean

added def Mathlib.Tactic.MkIff.List.init

added def Mathlib.Tactic.MkIff.constrToProp

added def Mathlib.Tactic.MkIff.listOptionMerge

added def Mathlib.Tactic.MkIff.mkAndList

added def Mathlib.Tactic.MkIff.mkExistsList

added def Mathlib.Tactic.MkIff.mkIffOfInductivePropImpl

added def Mathlib.Tactic.MkIff.mkOpList

added def Mathlib.Tactic.MkIff.mkOrList

added def Mathlib.Tactic.MkIff.nCasesProd

added def Mathlib.Tactic.MkIff.nCasesSum

added def Mathlib.Tactic.MkIff.splitThenConstructor

added def Mathlib.Tactic.MkIff.toCases

added def Mathlib.Tactic.MkIff.toInductive

Created test/MkIffOfInductive.lean

added inductive ReflTransGen

added structure foo2

added structure foo

added inductive test.is_true