Skip to main content

🍃 Time.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Compare.
Require Proto_alpha.Environment.Data_encoding.

Definition t : Set := Z.

Definition Included_S : Compare.S (t := t) := Compare.Z.

Definition op_eq : t t bool := Included_S.(Compare.S.op_eq).

Definition op_ltgt : t t bool := Included_S.(Compare.S.op_ltgt).

Definition op_lt : t t bool := Included_S.(Compare.S.op_lt).

Definition op_lteq : t t bool := Included_S.(Compare.S.op_lteq).

Definition op_gteq : t t bool := Included_S.(Compare.S.op_gteq).

Definition op_gt : t t bool := Included_S.(Compare.S.op_gt).

Definition compare : t t int := Included_S.(Compare.S.compare).

Definition equal : t t bool := Included_S.(Compare.S.equal).

Definition max : t t t := Included_S.(Compare.S.max).

Definition min : t t t := Included_S.(Compare.S.min).

Definition add (time : t) (diff : int64) : t :=
  Z.add time diff.

Definition diff_value (time1 time2 : t) : int64 :=
  Z.sub time2 time1.

Definition of_seconds (seconds : int64) : t :=
  seconds.

Definition to_seconds (time : t) : int64 :=
  time.

Parameter of_notation : string option t.

Parameter of_notation_exn : string t.

Parameter to_notation : t string.

Parameter encoding : Data_encoding.t t.

Parameter rfc_encoding : Data_encoding.t t.

Parameter pp_hum : Format.formatter t unit.