The book Term Rewriting and All That by Baader and Nipkow includes a lot of code in ML, I highly recommend it. The code is available online: https://www21.in.

The book Term Rewriting and All That by Baader and Nipkow includes a lot of code in ML, I highly recommend it. The code is available online: https://www21.in.tum.de/~nipkow/TRaAT/ https://www21.in.tum.de/~nipkow/TRaAT/ The book also contains many useful references, which I also recommend to check out for your other questions. Also, in my experience, logic programming languages like Prolog are especially useful for reasoning about term rewriting systems, because they provide built-in features such as unification, subsumption checks and implicit search and backtracking which are very useful when working with and reasoning about term rewriting systems.