Lean4
/-- Filter out duplicate rewrites, reflexive rewrites
or rewrites that have metavariables in the replacement expression. -/
@[specialize]
def filterRewrites {α} (e : Expr) (rewrites : Array α) (replacement : α → Expr) (makesNewMVars : α → Bool) :
MetaM (Array α) :=
withNewMCtxDepth
(do
let mut filtered := #[]
for rw in rewrites do
-- exclude rewrites that introduce new metavariables into the expression
if makesNewMVars rw then
continue
-- exclude a reflexive rewrite
if ← isExplicitEq (replacement rw) e then
trace[rw??]"discarded reflexive rewrite {replacement rw}"
continue
-- exclude two identical looking rewrites
if ← filtered.anyM (isExplicitEq (replacement rw) <| replacement ·) then
trace[rw??]"discarded duplicate rewrite {replacement rw}"
continue
filtered := filtered.push rw
return filtered)
