[isabelle-dev] code abbreviation for mapping over a fixed range
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 29 15:54:11 CET 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".
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.
> 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...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev