[Agda] fast gcd for Nat

[Matthew Daggitt]

Yes, feel free to open a PR with your suggestions.

On Thu, Mar 28, 2019 at 3:03 AM Guillaume Allais <
guillaume.allais at ens-lyon.org> wrote:

> Dear Sergei,
>
> 0.18 (or 1.0 as it is now known) is going to be released imminently
> together with Agda 2.6.0. I doubt very much that anything extra will
> get in before the deadline.
>
> I am very happy to hear that you now have safe versions of the fast
> functions. This is much more likely to get in as it won't break
> anything.
>
> Best,
> --
> gallais
>
> On 27/03/2019 18:56, Sergei Meshveliani wrote:
> > Dear all,
> >
> > I have implemented the following fast functions for Nat:
> > `compare', toDecimalSystem, show, gcd.
> >
> > They are certified (`TERMINATING' removed from `show').
> > There are used built-ins  % (`modulo'), _div_  of  Nat.DivMod.
> >
> > If similar things will not appear in lib-0.18, then, may be I would come
> > up the proposal.
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190328/0dc111ad/attachment.html>