Closed mtzguido closed 4 years ago
This was meant to reduce the clutter on printed terms, but our pretty printer is now smarter about it.
See also FStarLang/FStar#1869
Hey Clément. Any opinion on this PR? Thanks!
LGTM, thanks!
This was meant to reduce the clutter on printed terms, but our pretty printer is now smarter about it.
See also FStarLang/FStar#1869