package coq-gaia-schutte
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Implementation of ordinals in Coq following Schütte and Ackermann
Install
Dune Dependency
Authors
Maintainers
Sources
v1.14.tar.gz
sha512=aec8b3321bba4ffeedf65f2411f0154edc729df6b64b619cfffc46db275f58d1fdfe0e1923b191a9e5b35120e1ee3cf8fae8b0a8c4600278d6061a46cf7ecc74
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:2022-03-23Published: 25 Mar 2022
Dependencies (3)
-
coq-mathcomp-ssreflect
>= "1.12.0" & < "1.15~"
-
coq
>= "8.10" & < "8.16~"
-
dune
>= "2.5"
Dev Dependencies
None
Used by (2)
-
coq-gaia-hydras
>= "0.9"
-
coq-gaia-ordinals
< "1.15"
Conflicts (1)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page