show_ty should apply to binders in term_to_string

[robblanco]

Converting a term to a string via Term.term_to_string is informed by the show_* configuration variables. However, the type of bound variables in Lam is never shown if show_ty = true: not at the binder, not at each instance in the subterm.

It would be consistent, as well as useful, to extend the printer to all type annotations. For example, x\x should at least become something like $(x:i)\x.

[chaudhuri]

The $ notation is just for debugging, so feel free to add this.

However, I just realized that there is also the Set types on flag. If that is on, perhaps it should print it as x : i\ x instead. Maybe that is a bit excessive. Perhaps have a Set types verbose flag?

[robblanco]

Either way works for me. (x : i)\x would be closer to how one normally disambiguates types. I don't think this flag and the debugging variable share code, although in principle they could.

Would that be the only difference between Set types on and the proposed Set types verbose?

[chaudhuri]

This is now implemented in the ipfs branch that may be merged to master later.