> The new definition actually causes *more* allocation than the original > one, except for very short lists, because every call of @ copies its > first argument. Note that the code equation for [_..<_] is > > lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])" > > which has no calls to @ at all; a corresponding code equation for > a fused "map_upt f i j = map f [i..<j]" would be > > "map_upt f i j = if i < j then f i # map_upt f (Suc i) j else []" > > which could be used to define map_range: > > "map_range f n = map_upt f 0 n"
OK, I'll revert this.
Thanks for having an eye on that.
Florian
--
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
