Skip to main content

🍃 Bounded.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.

Module BOUNDS.
  Record signature {ocaml_type : Set} : Set := {
    ocaml_type := ocaml_type;
    min_value : ocaml_type;
    max_value : ocaml_type;
  }.
End BOUNDS.
Definition BOUNDS := @BOUNDS.signature.
Arguments BOUNDS {_}.

Module S.
  Record signature {t ocaml_type : Set} : Set := {
    t := t;
    ocaml_type := ocaml_type;
    min_value : ocaml_type;
    max_value : ocaml_type;
    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;
    pp : Format.formatter t unit;
    to_value : t ocaml_type;
    of_value : ocaml_type option t;
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _}.

Parameter Int64_t : (B : BOUNDS (ocaml_type := int64)), Set.

Parameter Int64 :
   (B : BOUNDS (ocaml_type := int64)),
  S (t := Int64_t B) (ocaml_type := int64).

Parameter Int32_t : (B : BOUNDS (ocaml_type := int32)), Set.

Parameter Int32 :
   (B : BOUNDS (ocaml_type := int32)),
  S (t := Int32_t B) (ocaml_type := int32).

Parameter Non_negative_int32_t : Set.

Parameter Non_negative_int32 :
  S (t := Non_negative_int32_t) (ocaml_type := int32).

Parameter Int31_t : (B : BOUNDS (ocaml_type := int)), Set.

Parameter Int31 :
   (B : BOUNDS (ocaml_type := int)),
  S (t := Int31_t B) (ocaml_type := int).

Parameter Int16_t : (B : BOUNDS (ocaml_type := int)), Set.

Parameter Int16 :
   (B : BOUNDS (ocaml_type := int)),
  S (t := Int16_t B) (ocaml_type := int).

Parameter Uint16_t : (B : BOUNDS (ocaml_type := int)), Set.

Parameter Uint16 :
   (B : BOUNDS (ocaml_type := int)),
  S (t := Uint16_t B) (ocaml_type := int).

Parameter Int8_t : (B : BOUNDS (ocaml_type := int)), Set.

Parameter Int8 :
   (B : BOUNDS (ocaml_type := int)),
  S (t := Int8_t B) (ocaml_type := int).

Parameter Uint8_t : (B : BOUNDS (ocaml_type := int)), Set.

Parameter Uint8 :
   (B : BOUNDS (ocaml_type := int)),
  S (t := Uint8_t B) (ocaml_type := int).