def
Lean.Elab.WF.simpMatchWF?
(info : Lean.Elab.WF.EqnInfo)
(us : List Lean.Level)
(fixedPrefix : Array Lean.Expr)
(mvarId : Lean.MVarId)
:
Simplify match
-expressions when trying to prove equation theorems for a recursive declaration defined using well-founded recursion.
It is similar to simpMatch?
, but is also tries to fold WellFounded.fix
applications occurring in discriminants.
See comment at tryToFoldWellFoundedFix
.
Instances For
def
Lean.Elab.WF.simpMatchWF?.pre
(info : Lean.Elab.WF.EqnInfo)
(us : List Lean.Level)
(fixedPrefix : Array Lean.Expr)
(e : Lean.Expr)
:
Instances For
Instances For
def
Lean.Elab.WF.registerEqnsInfo
(preDefs : Array Lean.Elab.PreDefinition)
(declNameNonRec : Lake.Name)
(fixedPrefixSize : Nat)
: