Return to Answer

clickable links

Source Link

edit approved Mar 7, 2022 at 20:53

This was changed in Coq 8.14 (MR: github.com/coq/coq/pull/14086https://github.com/coq/coq/pull/14086), and the changes are summarized in coq.inria.fr/refman/changes.html#id310https://coq.inria.fr/refman/changes.html#id310. Quoting:

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)

As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.

This was changed in Coq 8.14 (MR: github.com/coq/coq/pull/14086), and the changes are summarized in coq.inria.fr/refman/changes.html#id310. Quoting:

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)

As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.

This was changed in Coq 8.14 (MR: https://github.com/coq/coq/pull/14086), and the changes are summarized in https://coq.inria.fr/refman/changes.html#id310. Quoting:

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)

As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.

Source Link

created Feb 15, 2022 at 21:45

Blaisorblade

This was changed in Coq 8.14 (MR: github.com/coq/coq/pull/14086), and the changes are summarized in coq.inria.fr/refman/changes.html#id310. Quoting:

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)

As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.