[isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- From: Christian Sternagel <c.sternagel at gmail.com>
- Date: Thu, 24 Oct 2013 18:10:28 +0900
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0
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
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
More concretely, what is your advice for a function like
(('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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and