Equations
Instances For
def
Aesop.CtorNames.toInductionAltLHS
(cn : CtorNames)
:
Lean.TSyntax `Lean.Parser.Tactic.inductionAltLHS
Equations
Instances For
def
Aesop.CtorNames.toInductionAlt
(cn : CtorNames)
(tacticSeq : Array Lean.Syntax.Tactic)
:
Lean.TSyntax `Lean.Parser.Tactic.inductionAlt
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Aesop.ctorNamesToRCasesPats
(cns : Array CtorNames)
:
Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed
Equations
Instances For
def
Aesop.ctorNamesToInductionAlts
(cns : Array (CtorNames × Array Lean.Syntax.Tactic))
:
Lean.TSyntax `Lean.Parser.Tactic.inductionAlts