package rocq-formalv-time

  1. Overview
  2. Doc
A Rocq library for time and date arithmetic according to the UTC standard with leap seconds

Install

Dune Dependency

Authors

Maintainers

Sources

formalv-1.6.0.tar.gz
sha512=6126fcf580c61c718cb17f585f6c4a1c8171894c4c2809ec27a65e053d328994b7554081b4e7c79e4149c89f104e679f86ce37e6901de2c6fbddce57af546691

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 (9)

  1. rocq-formalv-check_range = version
  2. rocq-formalv-prim63_mathcomp = version
  3. rocq-mathcomp-algebra (>= "2.5.0" & < "2.6~")
  4. rocq-mathcomp-order (>= "2.5.0" & < "2.6~")
  5. rocq-mathcomp-boot (>= "2.5.0" & < "2.6~")
  6. rocq-stdlib (>= "9.0" & < "9.1~")
  7. coq-core (>= "9.0" & < "9.1~")
  8. rocq-core (>= "9.0" & < "9.1~")
  9. ocaml >= "4.10"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover