Skip to content

Gaia release for MathComp 1.14.0
Compare
Choose a tag to compare
@palmskog palmskog released this 23 Mar 11:24
· 23 commits to master since this release
v1.14
74133fe
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

This release is known to work with Coq 8.10 to 8.15 and MathComp 1.12.0 to 1.14.0. While the Coq content is the same as before, the release splits Gaia into the following packages for easier reuse:

  • coq-gaia-theory-of-sets: sets, cardinals, and integers following Bourbaki's Theory of Sets book
  • coq-gaia-schutte: independent syntactic formalization of ordinals following Schütte and Ackermann
  • coq-gaia-ordinals: implementation and properties of ordinals using set theory
  • coq-gaia-numbers: implementation of algebraic structures following Bourbaki, including Z, Q, and R
  • coq-gaia-stern: independent formalization of properties of Fibonacci numbers and the Stern diatomic sequence
Assets 2
Loading