Mario Xerxes Castelán Castro (Dec 28 2025 at 01:17): Mario Xerxes Castelán Castro (Dec 28 2025 at 01:17):Why is it that this does not work
fun my_divides :: "nat ⇒ nat ⇒ bool" where
"my_divides n m = ∃k. m = k * n"
but adding parentheses works
fun my_divides :: "nat ⇒ nat ⇒ bool" where
"my_divides n m = (∃k. m = k * n)"
?
Christian Pardillo Laursen (Jan 01 2026 at 17:54):Bindings often need parentheses to know their scope - parsing is done before type checking so it can't use the type information to know what scope would make sense, and here the equality has quite low precedence so I think it leads to ambiguity
Last updated: Jan 17 2026 at 20:25 UTC