[isabelle] partial function



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!
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.