[isabelle] Partial function simple question



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.