-
Notifications
You must be signed in to change notification settings - Fork 43
2021 03 26 Meeting
affeldt-aist edited this page Mar 26, 2021
·
1 revision
Participants: Marie, Kazuhiko, Pierre-Yves, Cyril, Reynald
- about https://github.com/math-comp/analysis/pull/334
- TODO: Marie does the dispatch and we will merged
-
dense
goes totopology.v
-
floor_nat_comp
should use ceiling (or trunc?) TODO: Reynald to give the pointer to Marie - definitions in sections should stay there with possibly a comment
- mention as a comment that this should be generalized to vector spaces?
- about https://github.com/math-comp/analysis/pull/337
- low priority because nobody using it at this point
- treatment of functions as predicate is different from what is done in the library
- should be uniformized
- many things can be reused from the library (e.g.,
contra
lemmas)
- about https://github.com/math-comp/analysis/pull/294
- might be heading for a merge despite that fact that improvements shall come later
- about https://github.com/math-comp/analysis/pull/311
- heading for a merge
- refactoring still need though, Cyril to look at it
- one issue is the notion of restriction it introduces which is competing with
fer
- should it use pointed types for
patch
?- so that
patch
does not take a default function anymore - but this approach is not without problems
- so that
- we should maybe adopt this definition
- specialize when we are on a ring, in the manner of
nth
which is specialized to0
- here, the zero would be the constant zero function
- specialize when we are on a ring, in the manner of
- TODO: try to replace
fer
by this PR definition
- heading for a merge
- about PR https://github.com/math-comp/analysis/pull/318
- might need to hear from the author
- status of PR https://github.com/math-comp/analysis/pull/116
- in progress
- status of PR https://github.com/math-comp/analysis/pull/180
- try to recompile it now that PR #205 has been merged
- heading for a merge
- about PR https://github.com/math-comp/analysis/pull/358
- the computational contents should not be relevant
- a priori no reason to use
Defined
instead ofQed
- test whether it is true and merge
- about issue https://github.com/math-comp/analysis/issues/348
- agree to use
bar R
instead of the notation{ereal R}
- agree to use
- merge the PR fixing issue https://github.com/math-comp/analysis/issues/323
- this is probably the result of a bad merge
- agree to release 0.3.7 asap
- TODO: try to schedule the next meeting at 2pm Paris Time