Rocq Call 2025 06 03 - rocq-prover/rocq GitHub Wiki

Topics

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.