mechvel

Fast modular arithmetic needs fast divMod, and fast divMod needs fast comparison

Currently standard library applies built-in arithmetic for Nat. If we take this, then there does not remain any performance question about modulo arithmetic. Because divMod works fast, "almost in constant...

May be, change this convention? On the other hand ``x|xy∧y|xy`` looks reasonable.

The most general construct here is a Fraction Domain over a (commutative?) Ring R by a Multiplicative system S in R, where the denominators for fractions over R are taken...

The `?' symbol meant ``What people think of this?''. 1. Exponentiation x ^ n in Monoid can be optimized to work faster at run time. i suggest this optimization. This...

Personally, I would like the divisibility definition in ``...RawMagma`` as it is in `lib-1.7.3` (and my project has a great number of this divisibility usage). Оn the other hand, the...

On 2024-04-14 22:29, G. Allais wrote: >> Because Nat._+_ and Nat._*_ are implemented as built-in, not in >> Agda. > > That is incorrect: these definitions are implemented in Agda,...

On 2024-04-15 00:11, Nathan van Doorn wrote: > You can click through to Agda.Buildin.Nat and see exactly the > definition you expected here [1] > I look into `lib-2.0` and...

(Sorry, probably this needs to be in Zulip) I do not say that Agda.BuiltIn is not needed. I am trying to show that one needs to avoid it in any...

It is even worse. The general definition for `_∣_` is not imported to Data.Nat.Divisibility.Core. Instead Nat...Core gives its own definition for `_∣_` in which the parts of `equality` are swapped.