search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

show_ty should apply to binders in term_to_string #85

Closed robblanco closed 1 year ago

robblanco commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 1 year ago

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