[isabelle-dev] code abbreviation for mapping over a fixed range

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 29 15:54:11 CET 2015

Hi Christian,

> This email refers to the following commit:
>   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
>   code abbreviation for mapping over a fixed range
> Is there a specific reason for this code equation:
>   "map_range f (Suc n) = map_range f n @ [f n]"
> It seems rather inefficient. Anyway, what's the purpose of "map_range".

the idea of map_range is to avoid building a list first and then mapping it.

Maybe this was though too short.  That changeset fell out of another
work and I just took it into the history without too much thinking about
it again.  Before reverting that (or replacing it by something better),
some concrete measurements could be helpful, though.


> cheers
> chris
> PS: I was confused about [code_abbrev], thus looked it up in isar-ref,
> then was further confused :D
>   "code_abbrev" declares (or with option “del” removes) equations which
>     are applied as rewrite rules to any result of an evaluation and
>     symmetrically during preprocessing to any code equation or
>     evaluation input.
> In my opinion the usage of the word "symmetrically" could be clarified.
> Does it mean "similar to the previous use case" or "symmetric in the
> sense of reading the equation from right to left"?


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151029/61dededf/attachment.sig>

More information about the isabelle-dev mailing list