Documentation

Lean.Meta.Tactic.Split

source
def Lean.Meta.Split.getSimpMatchContext:
Lean.MetaM Lean.Meta.Simp.Context
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatch (e : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatch.pre (e : Lean.Expr) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatchTarget (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.applyMatchSplitter (mvarId : Lean.MVarId) (matcherDeclName : Lean.Name) (us : Array Lean.Level) (params : Array Lean.Expr) (discrs : Array Lean.Expr) :
Lean.MetaM (List Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.splitMatch (mvarId : Lean.MVarId) (e : Lean.Expr) :
Lean.MetaM (List Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
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.

Equations
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
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.splitTarget? (mvarId : Lean.MVarId) (splitIte : optParam Bool true) :
Lean.MetaM (Option (List Lean.MVarId))
Equations
  • One or more equations did not get rendered due to their size.
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))
Equations
  • One or more equations did not get rendered due to their size.