Mutual induction

A rudimentary mutual induction tactic. Written with Claude Sonnet 4 assistance.

partial def splitConjunctions (mvarId : Lean.MVarId) (type : Lean.Expr) : Lean.MetaM (List Lean.MVarId)

def elabMutualInduction (A : Lean.Ident) : Lean.Elab.Tactic.TacticM Unit

Equations

• One or more equations did not get rendered due to their size.

partial def elabMutualInduction.lambdafyGoal (nmA : Lean.Name) (iA : Lean.InductiveVal) (g : Lean.MVarId) (tp : Lean.Expr) : Lean.MetaM Lean.Expr

def tacticMutual_induction_ : Lean.ParserDescr

mutual_induction Foo eliminates the mutual inductive family that Foo is part of.

Equations

• One or more equations did not get rendered due to their size.