🦏 Sc_rollup_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Module Address.
Definition prefix : string := "scr1".
Definition encoded_size : int := 37.
Definition decoded_prefix : string :=
String.String "001" ("v" ++ String.String "132" (String.String "217" "")).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_hash" in
let title := "A smart contract rollup address" in
let b58check_prefix := decoded_prefix in
let size_value := Some 20 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Module Address.
Definition prefix : string := "scr1".
Definition encoded_size : int := 37.
Definition decoded_prefix : string :=
String.String "001" ("v" ++ String.String "132" (String.String "217" "")).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Sc_rollup_hash" in
let title := "A smart contract rollup address" in
let b58check_prefix := decoded_prefix in
let size_value := Some 20 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Inclusion of the module [H]
Definition t := H.(S.HASH.t).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Init function; without side-effects in Coq
Definition init_module1 : unit :=
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Inclusion of the module [Path_encoding_Make_hex_include]
Definition to_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
Definition of_b58data (function_parameter : Base58.data)
: option H.(S.HASH.t) :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast H.(S.HASH.t) payload in
Some h_value
else None
end.
End Address.
Definition state_hash_prefix : string :=
String.String "017" (String.String "144" ("z" ++ String.String "202" "")).
Module State_hash.
Definition prefix : string := "scs1".
Definition encoded_size : int := 54.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "state_hash" in
let title := "The hash of the VM state of a smart contract rollup" in
let b58check_prefix := state_hash_prefix in
let size_value {A : Set} : option A :=
None in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
Definition of_b58data (function_parameter : Base58.data)
: option H.(S.HASH.t) :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast H.(S.HASH.t) payload in
Some h_value
else None
end.
End Address.
Definition state_hash_prefix : string :=
String.String "017" (String.String "144" ("z" ++ String.String "202" "")).
Module State_hash.
Definition prefix : string := "scs1".
Definition encoded_size : int := 54.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "state_hash" in
let title := "The hash of the VM state of a smart contract rollup" in
let b58check_prefix := state_hash_prefix in
let size_value {A : Set} : option A :=
None in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Inclusion of the module [H]
Definition t := H.(S.HASH.t).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Init function; without side-effects in Coq
Definition init_module2 : unit :=
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Inclusion of the module [Path_encoding_Make_hex_include]
Definition to_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
Definition context_hash_to_state_hash (h_value : Context_hash.t) : M? t :=
if Compare.Int.equal size_value Context_hash.size_value then
return? (of_bytes_exn (Context_hash.to_bytes h_value))
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Inductive unreachable : Set :=.
(* Axiom hash_bytes : forall {A : Set}, unreachable -> A. *)
(* Axiom hash_string : forall {A : Set}, unreachable -> A. *)
End State_hash.
Definition t : Set := Address.t.
Definition description : string :=
Pervasives.op_caret
"A smart contract rollup is identified by a base58 address starting with "
Address.prefix.
Definition error_description : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A smart contract rollup address must be a valid hash starting with '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"A smart contract rollup address must be a valid hash starting with '%s'.")
Address.prefix.
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
Definition context_hash_to_state_hash (h_value : Context_hash.t) : M? t :=
if Compare.Int.equal size_value Context_hash.size_value then
return? (of_bytes_exn (Context_hash.to_bytes h_value))
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Inductive unreachable : Set :=.
(* Axiom hash_bytes : forall {A : Set}, unreachable -> A. *)
(* Axiom hash_string : forall {A : Set}, unreachable -> A. *)
End State_hash.
Definition t : Set := Address.t.
Definition description : string :=
Pervasives.op_caret
"A smart contract rollup is identified by a base58 address starting with "
Address.prefix.
Definition error_description : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"A smart contract rollup address must be a valid hash starting with '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"A smart contract rollup address must be a valid hash starting with '%s'.")
Address.prefix.
Init function; without side-effects in Coq
Definition init_module3 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"rollup.invalid_smart_contract_rollup_address"
"Invalid smart contract rollup address" error_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid smart contract rollup address "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid smart contract rollup address %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "address" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_sc_rollup_address" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_sc_rollup_address" string loc_value).
Definition of_b58check (s_value : string)
: Pervasives.result Address.t string :=
let error_value {A : Set} (function_parameter : unit)
: Pervasives.result A string :=
let '_ := function_parameter in
Pervasives.Error
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid_sc_rollup_address "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid_sc_rollup_address %s") s_value) in
match Base58.decode s_value with
| Some data ⇒
match data with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let hash_value := cast Address.t payload in
return? hash_value
else error_value tt
end
| _ ⇒ error_value tt
end.
Definition pp : Format.formatter → Address.t → unit := Address.pp.
Definition encoding : Data_encoding.encoding Address.t :=
Data_encoding.def "rollup_address" (Some "A smart contract rollup address")
(Some description)
(Data_encoding.conv_with_guard Address.to_b58check of_b58check None
Data_encoding.string_value).
Definition rpc_arg : RPC_arg.arg Address.t :=
let construct := Address.to_b58check in
let destruct (hash_value : string) : Pervasives.result Address.t string :=
Result.map_error
(fun (function_parameter : string) ⇒
let '_ := function_parameter in
error_description) (of_b58check hash_value) in
RPC_arg.make (Some "A smart contract rollup address.") "sc_rollup_address"
destruct construct tt.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Cache_memory_helpers.string_size_gen Address.size_value).
Definition Staker := Signature.Public_key_hash.
Module Index.
Definition t : Set := Address.t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Address.t) (l_value : list string)
: list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string)
: M? (option Address.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Address.t := rpc_arg.
Definition encoding : Data_encoding.encoding Address.t := encoding.
Definition compare : Address.t → Address.t → int := Address.compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Module Number_of_ticks.
Definition Bounded_Int64_include :=
Bounded.Int64
(let min_value := 0 in
let max_value := Int64.max_int in
{|
Bounded.BOUNDS.min_value := min_value;
Bounded.BOUNDS.max_value := max_value
|}).
Error_monad.register_error_kind Error_monad.Permanent
"rollup.invalid_smart_contract_rollup_address"
"Invalid smart contract rollup address" error_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid smart contract rollup address "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid smart contract rollup address %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "address" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_sc_rollup_address" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_sc_rollup_address" string loc_value).
Definition of_b58check (s_value : string)
: Pervasives.result Address.t string :=
let error_value {A : Set} (function_parameter : unit)
: Pervasives.result A string :=
let '_ := function_parameter in
Pervasives.Error
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid_sc_rollup_address "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid_sc_rollup_address %s") s_value) in
match Base58.decode s_value with
| Some data ⇒
match data with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let hash_value := cast Address.t payload in
return? hash_value
else error_value tt
end
| _ ⇒ error_value tt
end.
Definition pp : Format.formatter → Address.t → unit := Address.pp.
Definition encoding : Data_encoding.encoding Address.t :=
Data_encoding.def "rollup_address" (Some "A smart contract rollup address")
(Some description)
(Data_encoding.conv_with_guard Address.to_b58check of_b58check None
Data_encoding.string_value).
Definition rpc_arg : RPC_arg.arg Address.t :=
let construct := Address.to_b58check in
let destruct (hash_value : string) : Pervasives.result Address.t string :=
Result.map_error
(fun (function_parameter : string) ⇒
let '_ := function_parameter in
error_description) (of_b58check hash_value) in
RPC_arg.make (Some "A smart contract rollup address.") "sc_rollup_address"
destruct construct tt.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Cache_memory_helpers.string_size_gen Address.size_value).
Definition Staker := Signature.Public_key_hash.
Module Index.
Definition t : Set := Address.t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Address.t) (l_value : list string)
: list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string)
: M? (option Address.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Address.t := rpc_arg.
Definition encoding : Data_encoding.encoding Address.t := encoding.
Definition compare : Address.t → Address.t → int := Address.compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Module Number_of_ticks.
Definition Bounded_Int64_include :=
Bounded.Int64
(let min_value := 0 in
let max_value := Int64.max_int in
{|
Bounded.BOUNDS.min_value := min_value;
Bounded.BOUNDS.max_value := max_value
|}).
Inclusion of the module [Bounded_Int64_include]
Definition t := Bounded_Int64_include.(Bounded.S.t).
Definition min_value := Bounded_Int64_include.(Bounded.S.min_value).
Definition max_value := Bounded_Int64_include.(Bounded.S.max_value).
Definition op_eq := Bounded_Int64_include.(Bounded.S.op_eq).
Definition op_ltgt := Bounded_Int64_include.(Bounded.S.op_ltgt).
Definition op_lt := Bounded_Int64_include.(Bounded.S.op_lt).
Definition op_lteq := Bounded_Int64_include.(Bounded.S.op_lteq).
Definition op_gteq := Bounded_Int64_include.(Bounded.S.op_gteq).
Definition op_gt := Bounded_Int64_include.(Bounded.S.op_gt).
Definition compare := Bounded_Int64_include.(Bounded.S.compare).
Definition equal := Bounded_Int64_include.(Bounded.S.equal).
Definition max := Bounded_Int64_include.(Bounded.S.max).
Definition min := Bounded_Int64_include.(Bounded.S.min).
Definition encoding := Bounded_Int64_include.(Bounded.S.encoding).
Definition pp := Bounded_Int64_include.(Bounded.S.pp).
Definition to_value := Bounded_Int64_include.(Bounded.S.to_value).
Definition of_value := Bounded_Int64_include.(Bounded.S.of_value).
Definition zero : t :=
match of_value 0 with
| Some zero ⇒ zero
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert t false
end.
End Number_of_ticks.
Definition min_value := Bounded_Int64_include.(Bounded.S.min_value).
Definition max_value := Bounded_Int64_include.(Bounded.S.max_value).
Definition op_eq := Bounded_Int64_include.(Bounded.S.op_eq).
Definition op_ltgt := Bounded_Int64_include.(Bounded.S.op_ltgt).
Definition op_lt := Bounded_Int64_include.(Bounded.S.op_lt).
Definition op_lteq := Bounded_Int64_include.(Bounded.S.op_lteq).
Definition op_gteq := Bounded_Int64_include.(Bounded.S.op_gteq).
Definition op_gt := Bounded_Int64_include.(Bounded.S.op_gt).
Definition compare := Bounded_Int64_include.(Bounded.S.compare).
Definition equal := Bounded_Int64_include.(Bounded.S.equal).
Definition max := Bounded_Int64_include.(Bounded.S.max).
Definition min := Bounded_Int64_include.(Bounded.S.min).
Definition encoding := Bounded_Int64_include.(Bounded.S.encoding).
Definition pp := Bounded_Int64_include.(Bounded.S.pp).
Definition to_value := Bounded_Int64_include.(Bounded.S.to_value).
Definition of_value := Bounded_Int64_include.(Bounded.S.of_value).
Definition zero : t :=
match of_value 0 with
| Some zero ⇒ zero
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert t false
end.
End Number_of_ticks.