Rocq Call 2025 06 03

• 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• Type@{s;u} instead of Type@{s|u}? (https://github.com/rocq-prover/rocq/pull/20635) (Gaëtan, 15min)
• design of named notation levels (draft: (https://github.com/proux01/rocq/blob/named-notation-level/design.md)) (Pierre, 20 min)

Roles

• Chairman: Nicolas
• Secretary: Théo
• Attending: Gaëtan, Pierre Roux, Théo, Nicolas

Notes

• Type@{s;u} instead of Type@{s|u}? (https://github.com/rocq-prover/rocq/pull/20635)
  • less ambiguous than the previous semantics
  • the PR adds a deprecation warning
  • Nicolas will review / merge the PR
• design of named notation levels (draft: (https://github.com/proux01/rocq/blob/named-notation-level/design.md))
  • Gaëtan raises the issue of an import of two libraries declaring levels that are unrelated (no constraints between them)
  • the proposed solution is to first Require the two libraries, then add the constraint between the levels, then Import the libraries to activate the parsing rules.
  • Discussion of the fact that the current parser supports several associativity rules at the same level, but usually this is not what we want.
  • Pierre may open an RFC and post it on Zulip to obtain more feedback.