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