Documentation

Lean.Meta.Tactic.Split

source
def Lean.Meta.Split.getSimpMatchContext :
Lean.MetaM Lean.Meta.Simp.Context
Instances For
    source
    def Lean.Meta.Split.simpMatch (e : Lean.Expr) :
    Lean.MetaM Lean.Meta.Simp.Result
    Instances For
      source
      def Lean.Meta.Split.simpMatch.pre (e : Lean.Expr) :
      Lean.Meta.SimpM Lean.Meta.Simp.Step
      Instances For
        source
        def Lean.Meta.Split.simpMatchTarget (mvarId : Lean.MVarId) :
        Lean.MetaM Lean.MVarId
        Instances For
          source
          def Lean.Meta.Split.applyMatchSplitter (mvarId : Lean.MVarId) (matcherDeclName : Lake.Name) (us : Array Lean.Level) (params : Array Lean.Expr) (discrs : Array Lean.Expr) :
          Lean.MetaM (List Lean.MVarId)
          Instances For
            source
            def Lean.Meta.Split.splitMatch (mvarId : Lean.MVarId) (e : Lean.Expr) :
            Lean.MetaM (List Lean.MVarId)
            Instances For
              source
              def Lean.Meta.Split.findSplit? (env : Lean.Environment) (e : Lean.Expr) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) :
              Option Lean.Expr

              Return an if-then-else or match-expr to split.

              Instances For
                source
                partial def Lean.Meta.Split.findSplit?.go (env : Lean.Environment) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) (e : Lean.Expr) :
                Option Lean.Expr
                source
                def Lean.Meta.Split.findSplit?.isCandidate (env : Lean.Environment) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) (e : Lean.Expr) :
                Bool
                Instances For
                  source
                  def Lean.Meta.splitTarget? (mvarId : Lean.MVarId) (splitIte : optParam Bool true) :
                  Lean.MetaM (Option (List Lean.MVarId))
                  Instances For
                    source
                    partial def Lean.Meta.splitTarget?.go (mvarId : Lean.MVarId) (splitIte : optParam Bool true) (target : Lean.Expr) (badCases : Lean.ExprSet) :
                    Lean.MetaM (Option (List Lean.MVarId))
                    source
                    def Lean.Meta.splitLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
                    Lean.MetaM (Option (List Lean.MVarId))
                    Instances For