Lean4
/-- Normalizes an expression, given initial data:
* `s`: a reference to the mutable `AtomM` state, for persisting across calls.
This ensures that atom ordering is used consistently.
* `cfg`: the configuration options
* `eval`: a normalization operation which will be run recursively, potentially dependent on a known
atom ordering
* `simp`: a cleanup operation which will be used to post-process expressions
* `tgt`: the expression to normalize
-/
def recurse (s : IO.Ref State) (cfg : Recurse.Config) (eval : Expr → AtomM Simp.Result)
(simp : Simp.Result → MetaM Simp.Result) (tgt : Expr) : MetaM Simp.Result := do
RecurseM.run s cfg eval simp <| onSubexpressions eval tgt
