traversing an expression making replacements

Stream: Is there code for X?

[Scott Morrison]

Do we have something of shape:

meta def foo (r : expr → tactic (expr × expr)) : expr → tactic (expr × expr) := sorry

such that if r e contains (e', prf) where prf : e = e', then foo r E replaces any subexpression e of E using the result of r e (when successful), returning eventually (E', P), where P : E = E'?

Basically analogous to the simplifier, except there are no lemmas, just an internal tactic that is deciding what it can rewrite. It seems such a basic bit of tooling that we must have this lying around already?

[Scott Morrison]

This is simplify_bottom_up (or simplify_top_down, depending on exactly how you interpret what I asked for), which is just a simple wrapper around ext_simplify_core.

[Anne Baanen]

norm_num uses docs#norm_num.derive' which is as you say a simple wrapper around ext_simplify_core