🍃 Bounded.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.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).
Parameter NonNegative_t : Set.
Parameter NonNegative : S (t := NonNegative_t).
End Int32.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.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).
Parameter NonNegative_t : Set.
Parameter NonNegative : S (t := NonNegative_t).
End Int32.