usability bug in squeeze_simp

Stream: general

[Johan Commelin]

@Simon Hudon If I run squeeze_simp [(mul_assoc _ _ _).symm], the output contains metavariables eq.symm (mul_assoc ?m_1 ?m_2 ?m_3).

[Johan Commelin]

Do you think you could postprocess to restore the _s?

[Simon Hudon]

I use pp to pretty print so it's not obvious. If I replace all with a constant named _, it comes out as «_» . I could try cleaning up after the pretty printing.

[Simon Hudon]

Actually, I think I'll just create a local_const with a unique name and then replace it with _ afterwards