[Agda] fast gcd for Nat

Sergei Meshveliani mechvel at botik.ru
Wed Mar 27 19:56:47 CET 2019


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  



More information about the Agda mailing list