2020 05 25 Meeting

participants: Cyril, Marie, Pierre-Yves, Reynald

• about PR 205
  • goal: get rid of ^o
    • by giving to numFieldTypes a canonical structure for normedModType
    • requires real-closed 1.1.0
    • the direct use of PseudoMetric.Pack might be the problem
• 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 \/ in sup_total
    • TODO: merge and then rebase the PR about Hahn-Banach to factorize
• 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 ereals form a PseudoMetricType completed
    • TODO: improve proofs (using wlog?)
  • TODO: prove lim_ereal_sup
• 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