Re: [isabelle] Partial function simple question



Hi Roger,

partial functions are actually normal functions that return an option value. So you can use plain function update fun_upd with syntax :=, i.e.,

f(2 := None)

is the same as function f except that 2 is mapped to None. Note that _(_ |-> _) is just a shorthand for _(_ := Some _).

Best,
Andreas

On 09/01/14 12:43, Roger H. wrote:
Hi,

i have

f :: nat ⇀ nat
f = [1 ↦ 0, 2 ↦ 5, 3 ↦ 7, ... , 100 ↦ 29]

and i want to write a new function g, which does the same as f, except it associates the number "2" to None, so it removes it from the list.

remove_two :: nat ⇀ nat
g = [1 ↦ 0, 3 ↦ 7, ... , 100 ↦ 29]

is there a way to do that?

Thank you!


  		 	   		





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