-
Notifications
You must be signed in to change notification settings - Fork 43
2020 05 25 Meeting
affeldt-aist edited this page May 25, 2020
·
1 revision
participants: Cyril, Marie, Pierre-Yves, Reynald
- about PR 205
- goal: get rid of
^o
- by giving to
numFieldType
s a canonical structure fornormedModType
- requires real-closed 1.1.0
- the direct use of
PseudoMetric.Pack
might be the problem
- by giving to
- goal: get rid of
- about PR 203
-
pred
vs.set
:- no final answer so far about
bool
vs.Prop
- some foresee some automation with SSReflect that could make the
use of
bool
transparent but that requires a large amount of work - the
\in
predicate is desirable - there might be an interest in keeping
||
instead of\/
insup_total
- TODO: merge and then rebase the PR about Hahn-Banach to factorize
- no final answer so far about
-
- about PR 180
- are joins lacking that would explain the need for extra typing notations?
- TODO: not all generalization have been done yet
- WANTED: a better name for
PseudoMetricNormedZmod
- about PR 189
- proof that
ereal
s form aPseudoMetricType
completed- TODO: improve proofs (using
wlog
?)
- TODO: improve proofs (using
- TODO: prove
lim_ereal_sup
- proof that
- release 3.0 ASAP
- at least, add a memo about the recent changes
- try to build a changelog out of the merged PRs
- TODO merge https://github.com/math-comp/analysis/pull/189