Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
> Dear @pi8027, I am afraid I will not have the time to review this PR this month since it is a pretty big one, and I would need the...
> > BTW, I came across a problem recently: I could not make `'I_n` a `finOrderType` for any `n` (not manifestly positive), because our phrasing of `finOrderType` inherits structures with...
I finished documentation and this PR is ready for review. But, we probably have to separate the finite counterparts off as `finorder.v` since `order.v` became too large (approx. 12k lines).
Since `(meet|join)Semilattice` is too long, I'm thinking about replacing them with `(meet|join)Order`, e.g., `meetOrderType`. Any opinion?
> (setq coq-indent-proofstart 0) > (setq coq-indent-modulestart 0) Those settings do not seem to work in the current master branch of PG. Is there anyone who can confirm it?
@Sobernard @CohenCyril @amahboubi Hello. I found this PR is useful for my study on intervals and QE. If you don't plan to rebase and fix this, may I rebase this...
Just not to forget to rework this PR, I assign myself.
Now I'm reworking this PR. I guess one of `NumArchiClosedField` and `RealClosedArchiField` should be renamed (`ArchiClosed` or `ClosedArchi`?). *EDIT: these "closed" stand for different notions of closedness so probably OK....
So this is the PR that needs linting and refactoring, right?
Could someone grant me write permission to directly push to here? > `ERROR: Permission to math-comp/analysis.git denied to pi8027.`