Email Gateway (Aug 19 2022 at 13:27): Email Gateway (Aug 19 2022 at 13:27):From: "Roger H." <s57076@hotmail.com>
Hi,
i understand the ↦ syntax for partial functions, but what happens if i write
f: nat ⇀ nat,
[1 ↦ 2, 1 ↦ 3]
this is not a function, but if u call
value "f 1", it returns 3, and if you do
definition f :: "nat ⇀ nat" where
"f ≡ [1 ↦ 2, 1 ↦ 3, 1 ↦ 2]"
value "f 1" returns 2 again
...should it not return an error since it is not a function anymore?
Thank you!
Email Gateway (Aug 19 2022 at 13:27):From: Peter Lammich <lammich@in.tum.de>
This syntax is just a shortcut for a sequence of function updates,
starting with the empty map. Thus, later updates just overwrite earlier
ones.
Last updated: Nov 21 2024 at 12:39 UTC