Skip to main content

🍃 Fitness.v

Environment

Gitlab , OCaml

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

Require Proto_alpha.Environment.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).