Skip to main content

🍃 Bounded.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Data_encoding.

Module Int32.
  Module BOUNDS.
    Record signature : Set := {
      min_int : int32;
      max_int : int32;
    }.
  End BOUNDS.
  Definition BOUNDS := BOUNDS.signature.

  Module S.
    Record signature {t : Set} : Set := {
      t := t;
      min_int : int32;
      max_int : int32;
      op_eq : t t bool;
      op_ltgt : t t bool;
      op_lt : t t bool;
      op_lteq : t t bool;
      op_gteq : t t bool;
      op_gt : t t bool;
      compare : t t int;
      equal : t t bool;
      max : t t t;
      min : t t t;
      encoding : Data_encoding.t t;
      to_int32 : t int32;
      of_int32 : int32 option t;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_}.

  Parameter Make_t : (B : BOUNDS), Set.

  Parameter Make : (B : BOUNDS), S (t := Make_t B).

End Int32.