package rocq-formalv-time
A Rocq library for time and date arithmetic according to the UTC standard with leap seconds
Install
Dune Dependency
Authors
Maintainers
Sources
formalv-1.5.0.tar.gz
sha512=2524a34502ac80cce0c51e7a7426ab48e445a35c305699a5d9e1b0d7b69ea04d91cc94acd8dad944b363f1bd58f57299009b386c74b8ef5fec883cf98e5d1a3c
Description
FV Time is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds (which are part of the UTC standard but usually not implemented in commercial libraries).
Dependencies (8)
-
rocq-formalv-check_range
= version -
rocq-formalv-prim63_mathcomp
= version -
rocq-mathcomp-algebra
(>= "2.5.0" & < "2.6~") -
rocq-mathcomp-order
(>= "2.5.0" & < "2.6~") -
rocq-mathcomp-boot
(>= "2.5.0" & < "2.6~") -
rocq-stdlib
(>= "9.0" & < "9.1~") -
coq-core
(>= "9.0" & < "9.1~") -
rocq-core
(>= "9.0" & < "9.1~")
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page