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 : Aesop.CtorNames) : Lean.TSyntax `rcasesPat

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• cn.toAltVarNames = { explicit := true, varNames := cn.args.toList }

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

Equations

• Aesop.CtorNames.mkFreshArgNames lctx cn = match Aesop.getUnusedNames lctx cn.args with | (args, lctx) => ({ ctor := cn.ctor, args := args, hasImplicitArg := cn.hasImplicitArg }, lctx)

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

Equations

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

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

Equations

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

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

Equations

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