Documentation

Lean.Meta.Tactic.SplitIf

source
opaque Lean.Meta.SplitIf.ext :
Lean.LazyInitExtension Lean.MetaM Lean.Meta.Simp.Context
source
def Lean.Meta.SplitIf.getSimpContext :
Lean.MetaM Lean.Meta.Simp.Context

Default Simp.Context for simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions.

Instances For
    source
    def Lean.Meta.SplitIf.discharge? (useDecide : optParam Bool false) :
    Lean.Meta.Simp.Discharge

    Default discharge? function for simpIf methods. It only uses hypotheses from the local context. It is effective after a case-split.

    Instances For
      source
      partial def Lean.Meta.SplitIf.findIfToSplit? (e : Lean.Expr) :
      Option Lean.Expr

      Return the condition of an if expression to case split.

      source
      def Lean.Meta.SplitIf.splitIfAt? (mvarId : Lean.MVarId) (e : Lean.Expr) (hName? : Option Lake.Name) :
      Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))
      Instances For
        source
        def Lean.Meta.simpIfTarget (mvarId : Lean.MVarId) (useDecide : optParam Bool false) :
        Lean.MetaM Lean.MVarId
        Instances For
          source
          def Lean.Meta.simpIfLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
          Lean.MetaM Lean.MVarId
          Instances For
            source
            def Lean.Meta.splitIfTarget? (mvarId : Lean.MVarId) (hName? : optParam (Option Lake.Name) none) :
            Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))
            Instances For
              source
              def Lean.Meta.splitIfLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (hName? : optParam (Option Lake.Name) none) :
              Lean.MetaM (Option (Lean.MVarId × Lean.MVarId))
              Instances For