Documentation

Lean.Meta.Tactic.Cases

def Lean.Meta.withNewEqs {α : Type} (targets targetsNew : Array Expr) (k : Array ExprArray ExprMetaM α) :
Equations
    Instances For
      partial def Lean.Meta.withNewEqs.loop {α : Type} (targets targetsNew : Array Expr) (k : Array ExprArray ExprMetaM α) (i : Nat) (newEqs newRefls : Array Expr) :
      def Lean.Meta.generalizeTargetsEq (mvarId : MVarId) (motiveType : Expr) (targets : Array Expr) :
      Equations
        Instances For
          Instances For

            Given a metavariable mvarId representing the goal

            Ctx |- T
            

            and an expression e : I A j, where I A j is an inductive datatype where A are parameters, and j the indices. Generate the goal

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

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

            If varName? is not none, it is used to name h'.

            Equations
              Instances For

                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

                Equations
                  Instances For
                    Instances For
                      partial def Lean.Meta.Cases.unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none) :
                      def Lean.Meta.Cases.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) :
                      Equations
                        Instances For
                          def Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array Meta.AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) :

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

                          • useNatCasesAuxOn is a temporary hack for the rcases family of tactics. Do not use it, as it is subject to removal. It enables using Nat.casesAuxOn instead of Nat.casesOn, which causes case splits on n : Nat to be represented as 0 and n' + 1 rather than as Nat.zero and Nat.succ n'.
                          Equations
                            Instances For

                              Keep applying cases on any hypothesis that satisfies p.

                              Equations
                                Instances For

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

                                  Equations
                                    Instances For

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

                                      Equations
                                        Instances For

                                          Auxiliary structure for storing byCases tactic result.

                                          Instances For

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

                                            Equations
                                              Instances For

                                                Given dec : Decidable p, split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.

                                                Equations
                                                  Instances For