Proof production algorithm

[vitrun]

Is it possible to extract the steps needed to produce the final answer?
for example.
(a*2)/2 -step1-> a*(2/2) -step2-> a

rule of step1: (x*y)/z --> x*(y/z)
rule of step2: x/x --> 1

[0x0f0f0f]

Not yet. We're planning to do so
Egg rust library has it
https://docs.rs/egg/0.7.1/egg/tutorials/_03_explanations/index.html

[0x0f0f0f]

See this for later implementation https://www.cs.upc.edu/~roberto/papers/rta05.pdf cc @Wilkenfeld