Documentation

Aesop.Script.CtorNames

Instances For
    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
                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
                    Equations
                      Instances For