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

Christian Sternagel c.sternagel at gmail.com
Mon Oct 19 12:08:03 CEST 2015

This email refers to the following commit:


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



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>

More information about the isabelle-dev mailing list