Re: [isabelle] Partial function simple question



Hallo,

for the sake of completeness, I for one prefer the following notation:

f |` (-{2})

This consists of two parts: f |` A is simply the restriction of the
(partial) function f to the set A, and -{2} is the complement of the set
{2}, i.e. I restrict f to the complement of {2}. This way, you can also
easily delete multiple entries at once.

Cheers,
Manuel


On 09/01/14 13:33, Andreas Lochbihler wrote:
> 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.