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)"
?
Last updated: Dec 28 2025 at 12:45 UTC