Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] partial function


view this post on Zulip 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!

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC