structure Aesop.CtorNames : Type

• ctor : Lean.Name
• args : Array Lean.Name
• hasImplicitArg : Bool

  Whether the constructor has at least one implicit argument.

def Aesop.CtorNames.toRCasesPat (cn : CtorNames) : Lean.TSyntax `rcasesPat

def Aesop.CtorNames.toInductionAltLHS (cn : CtorNames) : Lean.TSyntax `Lean.Parser.Tactic.inductionAltLHS

def Aesop.CtorNames.toInductionAlt (cn : CtorNames) (tacticSeq : Array Lean.Syntax.Tactic) : Lean.TSyntax `Lean.Parser.Tactic.inductionAlt

def Aesop.CtorNames.toAltVarNames (cn : CtorNames) : Lean.Meta.AltVarNames

def Aesop.CtorNames.mkFreshArgNames (lctx : Lean.LocalContext) (cn : CtorNames) : CtorNames × Lean.LocalContext

def Aesop.ctorNamesToRCasesPats (cns : Array CtorNames) : Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed

def Aesop.ctorNamesToInductionAlts (cns : Array (CtorNames × Array Lean.Syntax.Tactic)) : Lean.TSyntax `Lean.Parser.Tactic.inductionAlts

def Aesop.mkCtorNames (iv : Lean.InductiveVal) : Lean.CoreM (Array CtorNames)