Dear Coq users,
The Coq development team is proud to announce the immediate
availability of Coq 8.13.0:
The full list of changes is available at the following address
https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13
Highlights:
- Introduction of primitive persistent arrays in the core language,
implemented using imperative persistent arrays.
- Introduction of definitional proof irrelevance for the equality type
defined in the SProp sort.
- Many improvements to the handling of notations, including number
notations, recursive notations and notations with bindings. A new
algorithm chooses the most precise notation available to print an
expression, which might introduce changes in printing behavior.
Best,