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

[Florian Haftmann]

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,
	Florian

> 
> 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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>