Commit 2025-08-13 21:56 2320ef63

chore: deduplicate "recursively on atoms" code (#27649) This PR abstracts the "run recursively on atoms" method, implicit in ring_nf and atom_nf, for stand-alone use. The key function produced is

def Mathlib.Tactic.AtomM.recurse
    (s : IO.Ref AtomM.State)
    (cfg : AtomM.Recurse.Config)
    (eval : Expr → AtomM Simp.Result)
    (cleanup : Simp.Result → MetaM Simp.Result)
    (tgt : Expr) :
    MetaM Simp.Result 

which runs an input metaprogram (eval : Expr → AtomM Simp.Result) on an input expression tgt recursively: on each atom for the metaprogram eval, before packaging it as an atom, it finds the maximal subexpressions of that atom on which eval is applicable, and runs eval there too (and so on). Also rewrite ring_nf and atom_nf to use the abstracted method. The new tests are documenting existing behavior.