Documentation

Lean.Meta.Tactic.Cases

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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
        • One or more equations did not get rendered due to their size.
        Instances For
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.MVarId.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) (useNatCasesAuxOn : optParam 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
              • mvarId.cases majorFVarId givenNames useNatCasesAuxOn = Lean.Meta.Cases.cases mvarId majorFVarId givenNames useNatCasesAuxOn
              Instances For
                @[deprecated Lean.MVarId.cases]
                Equations
                Instances For

                  Keep applying cases on any hypothesis that satisfies p.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For