[Agda] fast gcd for Nat

[Guillaume Allais]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190327/5a4a6238/attachment.sig>