Michael Lan (Oct 23 2023 at 01:13): Michael Lan (Oct 23 2023 at 01:13):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.
Huỳnh Trần Khanh (Oct 23 2023 at 01:26): Michael Lan (Oct 23 2023 at 01:31):Thanks!
Notification Bot (Oct 23 2023 at 01:35):Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC