Hi! Is there a way to have Coq explicitly parenthesize expressions that it would otherwise omit due to the order of operations being implied already due to precedence/associativity rules? This might be useful, e.g., in demonstrating a proof of associativity.

Thanks!

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Jun 18 2024 at 21:01 UTC