coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Set Printing Parens

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Set Printing Parens
Date: Thu, 20 Feb 2020 11:00:32 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f181.google.com
Ironport-phdr: 9a23:B5a9RhIWK9JE7SfjWNmcpTZWNBhigK39O0sv0rFitYgeIvzxwZ3uMQTl6Ol3ixeRBMOHsq4C27Cd6vmxEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba59IRmsrgjdqMYajZZ/Jqs11xDEvmZGd+NKyGxnIl6egwzy7dqq8p559CRQtfMh98peXqj/Yq81U79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+76puVRTlhjsLOyI//WrKjMF7kaBVrw+7pxFnzIHaYI+bOvljcK3DYdwXXnBOUtpLWiFbHo+wc4kCAuwcNuhYtYn9oF4OoAOiCAa3BOPvyyRIhn/o0q05zu8sDQfG0xYmH90TrX/Zq8/6O7wSUeC016nIzSvMb/BM1Tjn7ojHaBYhruyWUbJxcMrR1UYvGhjKjlWVs4PlPjeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4IO1lDL7zl2wIUyJd2mVkF7e9CkEJ9XtyCULYd5XsQiQ2RwtCkmzb0Go5i7czYOyJQj3RLQdeGIc5WQ7h3/U+aROzF4i2xheLK7nRq+61avxfDhVsSyzV1ErTJFn8HSunwR0xHf8MuKR/tn8ku82DuC1hrf5vxHLEwpk6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk//Kn6+XjYrn/p5+cM5J4hhjwMqgzmcGzHP40MgcJX2ic9uS80KPs8VflT7VNi/06iqjZsJbEKsQHvqO1HRNZ34I55xu8DzqqyskUkHgGIV5fZR6KjJXlN0nLIP/iDPe/h1qskC1sx/DDJrDuGI7CLnjCkLf6fbZy9U1cxBApwtBZ/Z1UDKwOLOjyWk/wqNzYAQQ0MwOxw+n9CdV90pkSVn6IAq+cKK/Sq0OH5vozI+mQY48YoCryK/885/L3kXA5nUIdcrKy0JsMaHG4G+xmLF+DbXrthNcBC2YKsRAkQOzkkl3RGQJUMn21Ruc34iwxQNatCp6GTYSwipSA2j26F9tYfDYVJEqLFCLBfYWFQPcBa2q7JMZnnnRQXLKhSpQh2BLovQnzzbYhL+vI9QUXsJvi0J5+4OiFxkJ6ziB9E8nIizLFdGpzhG5dH2ZrjpA6mlR0zxK46YY9g/FcEoYNtfZAUwN/NJqFiuIjW4m0VQXGcdOEDl2hR4f+WGBjfpcK29YLJn1FNZCnhxHH0TCtBuZMxbOODZ0wtKnb2iqofpov+zP9zKAkymIebI5XL2T/3/xw8gHSA8jClEDLz6s=

Would it be easy to implement this feature in Coq to ignore all the associativity/precedence smarts and print all the parentheses explicitly?

It seems many people would like to use such a feature:

https://stackoverflow.com/questions/39843485/can-i-force-coq-to-print-parentheses/39848168

Unset Printing All is often not useful in these cases because it dumps too much information making things unreadable again.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] Set Printing Parens, Abhishek Anand, 02/20/2020
- Re: [Coq-Club] Set Printing Parens, Hugo Herbelin, 02/20/2020