Glad to see this getting play on here. Egg presents a very compelling algorithm and library for equational reasoning over syntax trees that I've been pretty fas

Glad to see this getting play on here. Egg presents a very compelling algorithm and library for equational reasoning over syntax trees that I've been pretty fascinated with over the past couple months. These e-graph data structures are in the heart of SMT solvers but giving easier access to end users and specializing the algorithm to the different needs of optimizing rewrites really changes the game. There's some cool applications linked on the site that I recommend people check out. A kind of neat thing about it being in rust is that you can compile to WASM to throw stuff on the web. I had a little demo of using egg to rewrite some category theory on my blog here https://www.philipzucker.com/rust-category/ https://www.philipzucker.com/rust-category/