🍃 Fitness.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_T : S.T (t := list bytes).
Definition t := Included_T.(S.T.t).
Definition op_eq : t → t → bool := Included_T.(S.T.op_eq).
Definition op_ltgt : t → t → bool := Included_T.(S.T.op_ltgt).
Definition op_lt : t → t → bool := Included_T.(S.T.op_lt).
Definition op_lteq : t → t → bool := Included_T.(S.T.op_lteq).
Definition op_gteq : t → t → bool := Included_T.(S.T.op_gteq).
Definition op_gt : t → t → bool := Included_T.(S.T.op_gt).
Definition compare : t → t → int := Included_T.(S.T.compare).
Definition equal : t → t → bool := Included_T.(S.T.equal).
Definition max : t → t → t := Included_T.(S.T.max).
Definition min : t → t → t := Included_T.(S.T.min).
Definition pp : Format.formatter → t → unit := Included_T.(S.T.pp).
Definition encoding : Data_encoding.t t := Included_T.(S.T.encoding).
Definition to_bytes : t → bytes := Included_T.(S.T.to_bytes).
Definition of_bytes : bytes → option t := Included_T.(S.T.of_bytes).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_T : S.T (t := list bytes).
Definition t := Included_T.(S.T.t).
Definition op_eq : t → t → bool := Included_T.(S.T.op_eq).
Definition op_ltgt : t → t → bool := Included_T.(S.T.op_ltgt).
Definition op_lt : t → t → bool := Included_T.(S.T.op_lt).
Definition op_lteq : t → t → bool := Included_T.(S.T.op_lteq).
Definition op_gteq : t → t → bool := Included_T.(S.T.op_gteq).
Definition op_gt : t → t → bool := Included_T.(S.T.op_gt).
Definition compare : t → t → int := Included_T.(S.T.compare).
Definition equal : t → t → bool := Included_T.(S.T.equal).
Definition max : t → t → t := Included_T.(S.T.max).
Definition min : t → t → t := Included_T.(S.T.min).
Definition pp : Format.formatter → t → unit := Included_T.(S.T.pp).
Definition encoding : Data_encoding.t t := Included_T.(S.T.encoding).
Definition to_bytes : t → bytes := Included_T.(S.T.to_bytes).
Definition of_bytes : bytes → option t := Included_T.(S.T.of_bytes).