math-comp
Wochoice
Motivation for this change
Adds a proof of Zorn's lemma, Hausdorff maximal principle and the well ordering principle. Contains a patch of contra that we may want to extract.
Checklist
- [ ] added corresponding entries in
CHANGELOG_UNRELEASED.md
- [ ] added corresponding documentation in the headers
Reference: How to document
Reminder to reviewers
- Read this Checklist
- Put a milestone if possible
- Check labels
Contains a patch of contra that we may want to extract.
Do you mean that it ought to be a different PR? (That may help the review process.)
I would not go so far as "ought to", the fix is quite trivial, but if you would prefer a different PR, I can do it.
the fix is quite trivial
Ok. Since there is a number of definitions that are added to contra.v and many canonicals, it didn't look trivial to me ^_^.
if you would prefer a different PR, I can do it.
I think that it is better (different concerns, two commits are maybe better also for the git log).
@Tragicus could you rephrase your commit message so as to make
Co-Authored-By: Georges Gonthier <[email protected]>
a single line separated from the title by a white line, and verbatim (otherwise github does not pick it up)
Argh, I accidentally merged this instead of https://github.com/math-comp/analysis/pull/1183 and I don't have push right on master to revert that, could someone do it, maybe @CohenCyril ?
Done with @affeldt-aist @Tragicus could you please reopen the PR, sorry again.