Skip to content

2020 05 25 Meeting

Jump to bottom
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 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
Clone this wiki locally