[Agda] fast gcd for Nat

[Matthew Daggitt]

Sorry I forgot to add, that it would probably be best if you added them one
at a time.

On Thu, Mar 28, 2019 at 1:54 PM Matthew Daggitt <matthewdaggitt at gmail.com>
wrote:

> 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/b650a367/attachment.html>