*To*: Christian Sternagel <c.sternagel at gmail.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 24 Oct 2013 11:57:01 +0200*In-reply-to*: <5268E404.9050304@gmail.com>*References*: <5268E404.9050304@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Christian,

Therefore, you have to switch to some other type. There are two options:

Best, Andreas On 24/10/13 11:10, Christian Sternagel wrote:

Dear all (especially Andreas ;)), is it possible to automatically get efficient code when code generating a function involving the "('a, 'b) map" type (i.e., "'a => 'b option"). If I import AFP/Containers I can have this for "('a, 'b) mapping" (which is a type-copy of "('a, 'b) map"). But in the actual formalization "('a, 'b) map" is more convenient to use since we have nice syntax like "m x" for lookup and "m (x |-> t)" for update. Since according to the user guide the above is possible w.r.t. "'a set", I was wondering what the obstacle is for "('a, 'b) map" (or maybe I just misunderstood something). More concretely, what is your advice for a function like match_list :: (('f, 'v) term * ('f, 'v) term) list => ('v => ('f, 'v) term option) => ('f, 'v) subst where "match_list E Map.empty" gives a matcher for all equations in "E". Would you change this to use "('v, ('f, 'v) term) mapping" instead, or is there a way to get efficient code as it is? Thanks in advance! cheers chris

**Follow-Ups**:**Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Florian Haftmann

**References**:**[isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Previous by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Cl-isabelle-users October 2013 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