pushStep — Mathlib

Lean4
/-- Try to rewrite using a `push` lemma. -/
def pushStep (head : Head) : Simp.Simproc := fun e => do
  let e_whnf ← whnf e
  let some e_head := Head.ofExpr? e_whnf |
    return Simp.Step.continue
  unless e_head == head do
    return Simp.Step.continue
  let thms := pushExt.getState (← getEnv)
  if let some r← Simp.rewrite? e thms { } "push" false then
      -- We return `.visit r` instead of `.continue r`, because in the case of a triple negation,
          -- after rewriting `¬ ¬ ¬ p` into `¬ p`, we may want to rewrite `¬ p` again.

    return Simp.Step.visit r
  if let some e := e_whnf.not? then
    pushNegBuiltin e
  else
    return Simp.Step.continue
Похожие утверждения