Documentation

Lean.Meta.Tactic.Cases

source
def Lean.Meta.getInductiveUniverseAndParams (type : Lean.Expr) :
Lean.MetaM (List Lean.Level × Array Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.generalizeTargetsEq (mvarId : Lean.MVarId) (motiveType : Lean.Expr) (targets : Array Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
  • One or more equations did not get rendered due to their size.
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

    • mvarId: the new goal
    • indicesFVarIds: j' ids
    • fvarId: h' id
    • numEqs: number of equations in the target
    Equations
    • One or more equations did not get rendered due to their size.
    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 Lean.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)
        Equations
        • One or more equations did not get rendered due to their size.
        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). giveNames contains user-facing names for each alternative.

        Equations
        source
        def Lean.Meta.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :
        Lean.MetaM (Array Lean.Meta.CasesSubgoal)
        Equations
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Lean.MVarId.casesAnd (mvarId : Lean.MVarId) :
        Lean.MetaM Lean.MVarId

        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.
        source
        def Lean.MVarId.substEqs (mvarId : Lean.MVarId) :
        Lean.MetaM (Option Lean.MVarId)

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

        Equations
        • One or more equations did not get rendered due to their size.
        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 Lean.Name (Lean.Name.mkStr1 "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.

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