[isabelle-dev] code abbreviation for mapping over a fixed range
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
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: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev