*To*: Roger H. <s57076 at hotmail.com>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Partial function simple question*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 9 Jan 2014 13:33:43 +0100*In-reply-to*: <DUB124-W51029F19FCFB8B967370E38FB00@phx.gbl>*References*: <DUB124-W51029F19FCFB8B967370E38FB00@phx.gbl>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hi Roger,

f(2 := None)

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!

**Follow-Ups**:**Re: [isabelle] Partial function simple question***From:*Manuel Eberl

**References**:**[isabelle] Partial function simple question***From:*Roger H .

- Previous by Date: [isabelle] Partial function simple question
- Next by Date: Re: [isabelle] datatype_new_compat requires sort type
- Previous by Thread: [isabelle] Partial function simple question
- Next by Thread: Re: [isabelle] Partial function simple question
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list