See now 9a51e4dfc5d9.
Florian
Am 12.11.2015 um 10:58 schrieb Jose Divasón:
> Hi Bertram, Christian and Bertram,
>
> I would like to put my two cents in this topic. I have done a simple
> experiment about this using my AFP entry about the QR decomposition,
> where a strong use of map_rang
Hi Bertram, Christian and Bertram,
I would like to put my two cents in this topic. I have done a simple
experiment about this using my AFP entry about the QR decomposition, where
a strong use of map_range is done.
With the current map_range definition, the computation of the QR
decomposition of a
> 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..
> which has no calls to @ at all; a corresponding code equa
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 @ [
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 s
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
