is there a way I can use rewrite to fill in constants in systems of equations, or does that require a match + rewrite combo? I'm looking for a rewrite rule that takes me from a structure like

[(= x 5)
 (= y (+ x 5))]

[(= x 5)
 (= y (+ 5 5))]

There's no official support for math but its something I've been meaning to add for a long time because for at least addition, subtraction, and multiplication its kinda straightforward.

Addition at least with whole numbers just involves partitioning the target number and lining those up with the arguments. If one of the arguments is ground/solved then its even less work.

But maybe this isn't what you're looking for?

Can you put the example in input/output terms?