🍃 Operation.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Operation_hash.
Module shell_header.
Record record : Set := Build {
branch : Block_hash.t }.
Definition with_branch branch (r : record) :=
Build branch.
End shell_header.
Definition shell_header := shell_header.record.
Parameter shell_header_encoding : Data_encoding.t shell_header.
Module t.
Record record : Set := Build {
shell : shell_header;
proto : bytes }.
Definition with_shell shell (r : record) :=
Build shell r.(proto).
Definition with_proto proto (r : record) :=
Build r.(shell) proto.
End t.
Definition t := t.record.
Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Operation_hash.t).
Definition op_eq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_eq).
Definition op_ltgt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_ltgt).
Definition op_lt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_lt).
Definition op_lteq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_lteq).
Definition op_gteq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_gteq).
Definition op_gt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_gt).
Definition compare : t → t → int := Included_HASHABLE.(S.HASHABLE.compare).
Definition equal : t → t → bool := Included_HASHABLE.(S.HASHABLE.equal).
Definition max : t → t → t := Included_HASHABLE.(S.HASHABLE.max).
Definition min : t → t → t := Included_HASHABLE.(S.HASHABLE.min).
Definition pp : Format.formatter → t → unit :=
Included_HASHABLE.(S.HASHABLE.pp).
Definition encoding : Data_encoding.t t :=
Included_HASHABLE.(S.HASHABLE.encoding).
Definition to_bytes : t → bytes := Included_HASHABLE.(S.HASHABLE.to_bytes).
Definition of_bytes : bytes → option t :=
Included_HASHABLE.(S.HASHABLE.of_bytes).
Definition hash_value : t → Operation_hash.t :=
Included_HASHABLE.(S.HASHABLE.hash_value).
Definition hash_raw : bytes → Operation_hash.t :=
Included_HASHABLE.(S.HASHABLE.hash_raw).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Block_hash.
Require TezosOfOCaml.Environment.Structs.V0.Operation_hash.
Module shell_header.
Record record : Set := Build {
branch : Block_hash.t }.
Definition with_branch branch (r : record) :=
Build branch.
End shell_header.
Definition shell_header := shell_header.record.
Parameter shell_header_encoding : Data_encoding.t shell_header.
Module t.
Record record : Set := Build {
shell : shell_header;
proto : bytes }.
Definition with_shell shell (r : record) :=
Build shell r.(proto).
Definition with_proto proto (r : record) :=
Build r.(shell) proto.
End t.
Definition t := t.record.
Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Operation_hash.t).
Definition op_eq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_eq).
Definition op_ltgt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_ltgt).
Definition op_lt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_lt).
Definition op_lteq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_lteq).
Definition op_gteq : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_gteq).
Definition op_gt : t → t → bool := Included_HASHABLE.(S.HASHABLE.op_gt).
Definition compare : t → t → int := Included_HASHABLE.(S.HASHABLE.compare).
Definition equal : t → t → bool := Included_HASHABLE.(S.HASHABLE.equal).
Definition max : t → t → t := Included_HASHABLE.(S.HASHABLE.max).
Definition min : t → t → t := Included_HASHABLE.(S.HASHABLE.min).
Definition pp : Format.formatter → t → unit :=
Included_HASHABLE.(S.HASHABLE.pp).
Definition encoding : Data_encoding.t t :=
Included_HASHABLE.(S.HASHABLE.encoding).
Definition to_bytes : t → bytes := Included_HASHABLE.(S.HASHABLE.to_bytes).
Definition of_bytes : bytes → option t :=
Included_HASHABLE.(S.HASHABLE.of_bytes).
Definition hash_value : t → Operation_hash.t :=
Included_HASHABLE.(S.HASHABLE.hash_value).
Definition hash_raw : bytes → Operation_hash.t :=
Included_HASHABLE.(S.HASHABLE.hash_raw).