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
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
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
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,
