Hi Florian, > > 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.
Please don't forget about this. 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" Cheers, Bertram _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
