Value.into_str() is not well written (redundancies) and not well tested. It should be, in order to clarify what is expected in several different cases (whether or not \text{} should wrap the value etc.).
Log in to post a comment.