New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Deprecate NDefOps and NIso #18668
Deprecate NDefOps and NIso #18668
Conversation
@coqbot run full ci |
Indeed, maybe more results for logicians than for a stdlib. |
fe09144
to
912e73b
Compare
These files are not used in the stdlib, it's unlikely they are very useful to anyone. - `Numbers.Natural.Abstract.NDefOps` defines some operations on an abstract Natural domain; the operations should be defined in the corresponding implementations instead. - `Numbers.Natural.Abstract.NIso` studies isomorphisms between models of NAxioms, this is very rarely (if at all) used.
912e73b
to
4f81d36
Compare
Apparently, the refman compilation failure was due to the faulty indentation of the changelog of #18564 (cc @andres-erbsen FYI) but only showed up now, when adding something below in the same item list. |
@coqbot merge now |
@proux01: You cannot merge this PR because:
|
@coqbot merge now |
@proux01: You can't merge the PR because it hasn't been approved yet. |
@coqbot merge now |
Thank you very much! |
@Villetaneuse: You cannot merge this PR because:
|
These files are not used in the stdlib, it's unlikely they are very useful to anyone.
Numbers.Natural.Abstract.NDefOps
defines some operations on an abstract Natural domain; the operations should be defined in the corresponding implementations instead.Numbers.Natural.Abstract.NIso
studies isomorphisms between models of NAxioms, this is very rarely (if at all) used.