Email Gateway (Aug 19 2022 at 13:28): Email Gateway (Aug 19 2022 at 13:28):From: "Roger H." <s57076@hotmail.com>
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!
Email Gateway (Aug 19 2022 at 13:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 13:29):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Apr 20 2024 at 08:16 UTC