Coq 8.13.0 is out
Submitted by Enrico Tassi on January 7th, 2021
The Coq development team is proud to announce the immediate availability of Coq 8.13.0
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.
Please see the changelog to learn more about this release.