Lean4
/-- Try to rewrite using a `pull` lemma. -/
def pullStep (head : Head) : Simp.Simproc := fun e => do
let thms :=
pullExt.getState
(← getEnv)
-- We can't use `Simp.rewrite?` here, because we need to only allow rewriting with theorems
-- that pull the correct head.
let candidates ← Simp.withSimpIndexConfig <| thms.getMatchWithExtra e
if candidates.isEmpty then
return Simp.Step.continue
let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.1.priority > e₂.1.1.priority
for ((thm, thm_head), numExtraArgs) in candidates do
if thm_head == head then
if let some result← Simp.tryTheoremWithExtraArgs? e thm numExtraArgs then
return Simp.Step.continue result
return Simp.Step.continue
