def Lean.Meta.rwIfWith (hc e : Expr) : MetaM Simp.Result

Tries to rewrite the ite, dite or cond expression e with the hypothesis hc. If it fails, it returns a rewrite with proof? := none and unchaged expression.

Equations

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

def Lean.Meta.rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result

In the onAlt handler of a MatcherApp.transform, you can use this function on a properly substituted matcher application with the alternative altIdx.

If it fails, it returns a rewrite with proof? := none and the unchanged expression.

"Properly substituted" here means that the discriminants have been substituted according to the alternative; otherwise, the rewrite might fail because some hypothesis of the congruence equation theorem cannot be discharged by assumption or reflixivity. See Lean.Meta.Tactic.FunInd.buildInductionBody and Lean.Elab.Tactic.Do.VCGen.Split for examples of how to coerce MatherApp.transform into doing the substitution on the motive for you.

Equations

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