Documentation

Aesop.Script.CtorNames

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.
Equations
  • cn.toAltVarNames = { explicit := true, varNames := cn.args.toList }
Equations
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.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.