The topics of the next MathComp meeting are taken from this list. Please append your topic:

• let's put real_closed into MathComp?

• https://github.com/math-comp/math-comp/pull/1581 and https://github.com/math-comp/math-comp/pull/1582

• #[local] Lemma or #[local] Fact and Let

• About #1456 (lra/nra/psatz/ring/field without Stdlib) should we have a field by tac (:= by field?; tac without the warning) variant

• #1586 Documented but missing notations

• PR/issue triaging:

  • generalized of closure of an open interval (https://github.com/math-comp/analysis/pull/1910)
    • by PR https://github.com/math-comp/analysis/pull/1848
    • is_endless_porderType, etc.
  • Documentation on the necessity to use an explicit scalar law s in {linear _ -> _ | s}, see https://github.com/math-comp/analysis/pull/1913
  • generalize RHS and LHS: https://github.com/math-comp/math-comp/issues/1555
  • Split order.v: https://github.com/math-comp/math-comp/pull/1580
    • this one has a pretty long TODO list and looking for volunteers
    • Remove [POrder of T by <:] and [Order of T by <:] https://github.com/math-comp/math-comp/issues/1583 https://github.com/math-comp/math-comp/pull/1584
    • Also, eventually remove the suborder instances on sub_type?
  • Archimedean lemmas: https://github.com/math-comp/math-comp/pull/1510
    • find a new name for the old Archimedean mixin (now a factory) NumDomain_hasFloorCeilTruncn
    • find a new name for truncnD so that we can add the symmetric one

• Recruiting:

  • Wanted: someone to do the frequent backports from mathcomp-analysis / unstable.v

• bullet, indentation, controlling number of resulting goals... (again)

- any sensible way to introduce a disjoint union "operator"? (Re: https://github.com/math-comp/analysis/issues/1914)

https://rendez-vous.renater.fr/zw4q6-f243e-tsmlq https ://webinaire.numerique.gouv.fr/meeting/signin/invite/74330/creator/23124/hash/390ff5dc3d08630a3a56d9d890075e2f666b202c

(if the meeting has not started yet, please wait a few minutes)

Instructions to join the meeting (old instructions?)

• Chair: Cyril (leading the meeting, to be decided at each meeting for the next one, should send the reminder / cancel if no topics)
• Secretary: Reynald (taking notes, can be decided at the beginning of the meeting)