Open amirlb opened 1 month ago
actually this script doesn't work right now, it should be fixed first
Opened #501 to track export_equations
breakage.
Actually, this should still be open. AllEquations.lean is gone, but we should still move all scripts to use export_equations
.
OK, thanks for clarifying; I am reopening.
Instead they should use the
export_equations
script's output