package coq-formalv-time

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

Install

Dune Dependency

Authors

Maintainers

Sources

formalv-1.3.1.tar.gz
sha256=240a0294bfa990b4261662a86cf53bce44cd31672bbc69a9a3e667db5cc66ace

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

  1. coq-formalv-check_range = version
  2. coq-formalv-prim63_mathcomp = version
  3. coq-mathcomp-algebra (>= "2.3.0" & < "2.4~")
  4. coq-mathcomp-ssreflect (>= "2.3.0" & < "2.4~")
  5. coq (>= "8.20" & < "8.21~")

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover