Documentation

Lean.Meta.Tactic.Cases

source
def Lean.Meta.getInductiveUniverseAndParams (type : Lean.Expr) :
Lean.MetaM (List Lean.Level × Array Lean.Expr)
Instances For
    source
    def Lean.Meta.generalizeTargetsEq (mvarId : Lean.MVarId) (motiveType : Lean.Expr) (targets : Array Lean.Expr) :
    Lean.MetaM Lean.MVarId
    Instances For
      source
      structure Lean.Meta.GeneralizeIndicesSubgoal :
      Type
      Instances For
        source
        def Lean.Meta.generalizeIndices (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
        Lean.MetaM Lean.Meta.GeneralizeIndicesSubgoal

        Similar to generalizeTargets but customized for the casesOn motive. Given a metavariable mvarId representing the

        Ctx, h : I A j, D |- T

        where fvarId is hs id, and the type I A j is an inductive datatype where A are parameters, and j the indices. Generate the goal

        Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T

        Remark: (j == j' -> h == h') is a "telescopic" equality. Remark: j is sequence of terms, and j' a sequence of free variables. The result contains the fields

        Instances For
          source
          structure Lean.Meta.CasesSubgoalextends Lean.Meta.InductionSubgoal :
          Type
          Instances For
            source
            structure Lean.Meta.Cases.Context :
            Type
            Instances For
              source
              partial def Lean.Meta.Cases.unifyEqs? (numEqs : Nat) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (caseName? : optParam (Option Lake.Name) none) :
              Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))
              source
              def Lean.Meta.Cases.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :
              Lean.MetaM (Array Lean.Meta.CasesSubgoal)
              Instances For
                source
                def Lean.MVarId.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :
                Lean.MetaM (Array Lean.Meta.CasesSubgoal)

                Apply casesOn using the free variable majorFVarId as the major premise (aka discriminant). givenNames contains user-facing names for each alternative.

                Instances For
                  source
                  @[deprecated Lean.MVarId.cases]
                  def Lean.Meta.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :
                  Lean.MetaM (Array Lean.Meta.CasesSubgoal)
                  Instances For
                    source
                    def Lean.MVarId.casesRec (mvarId : Lean.MVarId) (p : Lean.LocalDecl → Lean.MetaM Bool) :
                    Lean.MetaM (List Lean.MVarId)

                    Keep applying cases on any hypothesis that satisfies p.

                    Instances For
                      source
                      def Lean.MVarId.casesAnd (mvarId : Lean.MVarId) :
                      Lean.MetaM Lean.MVarId

                      Applies cases (recursively) to any hypothesis of the form h : p ∧ q.

                      Instances For
                        source
                        def Lean.MVarId.substEqs (mvarId : Lean.MVarId) :
                        Lean.MetaM (Option Lean.MVarId)

                        Applies cases to any hypothesis of the form h : r = s.

                        Instances For
                          source
                          structure Lean.Meta.ByCasesSubgoal :
                          Type

                          Auxiliary structure for storing byCases tactic result.

                          Instances For
                            source
                            def Lean.MVarId.byCases (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : optParam Lake.Name `h) :
                            Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)

                            Split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.

                            Instances For