package coq-gaia-schutte
Implementation of ordinals in Coq following Schütte and Ackermann
Install
Dune Dependency
Authors
Maintainers
Sources
v2.4.tar.gz
sha512=6dd168dc3269cfaba4618e4d8cd22e108103ca814658c337a917df315180653e28aa89e2a7025fa0b478c083ecb2f0fe5148d3c4b9527f1c9c5227737f66f827
Description
Types for ordinal numbers in Coq using the Mathematical Components library, following the approaches of Schütte and Ackermann.
Tags
category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordinal arithmetic keyword:ordinal numbers logpath:gaia.schutte date:2024-07-24Published: 24 Jul 2026
Dependencies (3)
-
coq-mathcomp-ssreflect
>= "2.0" -
coq
>= "8.16" -
dune
>= "3.5"
Dev Dependencies
None
Used by (1)
-
coq-gaia-ordinals
>= "2.4"
Conflicts (1)
On This Page