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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
