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

[Christian Sternagel]

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

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151019/2c408b85/attachment.asc>