Documentation

Aesop.Script.CtorNames

source
structure Aesop.CtorNames :
Type
Instances For
    source
    def Aesop.CtorNames.toRCasesPat (cn : CtorNames) :
    Lean.TSyntax `rcasesPat
    Instances For
      source
      def Aesop.CtorNames.toInductionAltLHS (cn : CtorNames) :
      Lean.TSyntax `Lean.Parser.Tactic.inductionAltLHS
      Instances For
        source
        def Aesop.CtorNames.toInductionAlt (cn : CtorNames) (tacticSeq : Array Lean.Syntax.Tactic) :
        Lean.TSyntax `Lean.Parser.Tactic.inductionAlt
        Instances For
          source
          def Aesop.CtorNames.toAltVarNames (cn : CtorNames) :
          Lean.Meta.AltVarNames
          Instances For
            source
            def Aesop.CtorNames.mkFreshArgNames (lctx : Lean.LocalContext) (cn : CtorNames) :
            CtorNames × Lean.LocalContext
            Instances For
              source
              def Aesop.ctorNamesToRCasesPats (cns : Array CtorNames) :
              Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed
              Instances For
                source
                def Aesop.ctorNamesToInductionAlts (cns : Array (CtorNames × Array Lean.Syntax.Tactic)) :
                Lean.TSyntax `Lean.Parser.Tactic.inductionAlts
                Instances For
                  source
                  def Aesop.mkCtorNames (iv : Lean.InductiveVal) :
                  Lean.CoreM (Array CtorNames)
                  Instances For