🍃 Environment_modules.v
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import Proto_alpha.Environment.Variant.
Module Type Pervasives_signature.
Parameter raise : ∀ {a : Set}, extensible_type → a.
Parameter raise_notrace : ∀ {a : Set}, extensible_type → a.
Parameter invalid_arg : ∀ {a : Set}, string → a.
Parameter failwith : ∀ {a : Set}, string → a.
Parameter not : bool → bool.
Parameter op_andand : bool → bool → bool.
Parameter op_pipepipe : bool → bool → bool.
Parameter __LOC__ : string.
Parameter __FILE__ : string.
Parameter __LINE__ : int.
Parameter __MODULE__ : string.
Parameter __POS__ : string × int × int × int.
Parameter __LOC_OF__ : ∀ {a : Set}, a → string × a.
Parameter __LINE_OF__ : ∀ {a : Set}, a → int × a.
Parameter __POS_OF__ : ∀ {a : Set}, a → (string × int × int × int) × a.
Parameter op_pipegt : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_atat : ∀ {a b : Set}, (a → b) → a → b.
Parameter op_tildeminus : int → int.
Parameter op_tildeplus : int → int.
Parameter succ : int → int.
Parameter pred : int → int.
Parameter op_plus : int → int → int.
Parameter op_minus : int → int → int.
Parameter op_star : int → int → int.
Parameter op_div : int → int → int.
Parameter _mod : int → int → int.
Parameter abs : int → int.
Parameter max_int : int.
Parameter min_int : int.
Parameter land : int → int → int.
Parameter lor : int → int → int.
Parameter lxor : int → int → int.
Parameter lnot : int → int.
Parameter lsl : int → int → int.
Parameter lsr : int → int → int.
Parameter asr : int → int → int.
Parameter op_caret : string → string → string.
Parameter int_of_char : ascii → int.
Parameter char_of_int : int → ascii.
Parameter ignore : ∀ {a : Set}, a → unit.
Parameter string_of_bool : bool → string.
Parameter bool_of_string_opt : string → option bool.
Parameter string_of_int : int → string.
Parameter int_of_string_opt : string → option int.
Parameter fst : ∀ {a b : Set}, a × b → a.
Parameter snd : ∀ {a b : Set}, a × b → b.
Parameter op_at : ∀ {a : Set}, list a → list a → list a.
Module ref.
Record record {a : Set} : Set := Build {
contents : a;
}.
Arguments record : clear implicits.
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a contents.
End ref.
Definition ref := ref.record.
Parameter ref_value : ∀ {a : Set}, a → ref a.
Parameter op_exclamation : ∀ {a : Set}, ref a → a.
Parameter op_coloneq : ∀ {a : Set}, ref a → a → unit.
Parameter incr : ref int → unit.
Parameter decr : ref int → unit.
Inductive result (a b : Set) : Set :=
| Ok : a → result a b
| Error : b → result a b.
Arguments Ok {_ _}.
Arguments Error {_ _}.
Definition format6 (a b c d e f : Set) : Set :=
CamlinternalFormatBasics.format6 a b c d e f.
Definition format4 (a b c d : Set) : Set := format6 a b c c c d.
Definition format (a b c : Set) : Set := format4 a b c c.
Parameter string_of_format : ∀ {a b c d e f : Set},
format6 a b c d e f → string.
Parameter format_of_string : ∀ {a b c d e f : Set},
format6 a b c d e f → format6 a b c d e f.
Parameter op_caretcaret : ∀ {a b c d e f g h : Set},
format6 a b c d e f → format6 f b c e g h → format6 a b c d g h.
End Pervasives_signature.
Require Export Proto_alpha.Environment.Pervasives.
Module Pervasives_check : Pervasives_signature := Pervasives.
Module Type Either_signature.
Inductive t (a b : Set) : Set :=
| Left : a → t a b
| Right : b → t a b.
Arguments Left {_ _}.
Arguments Right {_ _}.
Parameter equal : ∀ {a b : Set},
(a → a → bool) → (b → b → bool) → t a b → t a b → bool.
Parameter compare : ∀ {a b : Set},
(a → a → int) → (b → b → int) → t a b → t a b → int.
End Either_signature.
Require Export Proto_alpha.Environment.Either.
Module Either_check : Either_signature := Either.
Module Type String_signature.
Parameter length : string → int.
Parameter get : string → int → ascii.
Parameter make : int → ascii → string.
Parameter init_value : int → (int → ascii) → string.
Parameter sub : string → int → int → string.
Parameter blit : string → int → bytes → int → int → unit.
Parameter concat : string → list string → string.
Parameter iter : (ascii → unit) → string → unit.
Parameter iteri : (int → ascii → unit) → string → unit.
Parameter map : (ascii → ascii) → string → string.
Parameter mapi : (int → ascii → ascii) → string → string.
Parameter trim : string → string.
Parameter escaped : string → string.
Parameter index_opt : string → ascii → option int.
Parameter rindex_opt : string → ascii → option int.
Parameter index_from_opt : string → int → ascii → option int.
Parameter rindex_from_opt : string → int → ascii → option int.
Parameter contains : string → ascii → bool.
Parameter contains_from : string → int → ascii → bool.
Parameter rcontains_from : string → int → ascii → bool.
Parameter uppercase_ascii : string → string.
Parameter lowercase_ascii : string → string.
Parameter capitalize_ascii : string → string.
Parameter uncapitalize_ascii : string → string.
Definition t : Set := string.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter split_on_char : ascii → string → list string.
End String_signature.
Require Export Proto_alpha.Environment.String.
Module String_check : String_signature := String.
Module Type Char_signature.
Parameter code : ascii → int.
Parameter chr : int → ascii.
Parameter escaped : ascii → string.
Parameter lowercase_ascii : ascii → ascii.
Parameter uppercase_ascii : ascii → ascii.
Definition t : Set := ascii.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Char_signature.
Require Export Proto_alpha.Environment.Char.
Module Char_check : Char_signature := Char.
Module Type Bytes_signature.
Parameter length : bytes → int.
Parameter get : bytes → int → ascii.
Parameter set : bytes → int → ascii → unit.
Parameter make : int → ascii → bytes.
Parameter init_value : int → (int → ascii) → bytes.
Parameter empty : bytes.
Parameter copy : bytes → bytes.
Parameter of_string : string → bytes.
Parameter to_string : bytes → string.
Parameter sub : bytes → int → int → bytes.
Parameter sub_string : bytes → int → int → string.
Parameter extend : bytes → int → int → bytes.
Parameter fill : bytes → int → int → ascii → unit.
Parameter blit : bytes → int → bytes → int → int → unit.
Parameter blit_string : string → int → bytes → int → int → unit.
Parameter concat : bytes → list bytes → bytes.
Parameter cat : bytes → bytes → bytes.
Parameter iter : (ascii → unit) → bytes → unit.
Parameter iteri : (int → ascii → unit) → bytes → unit.
Parameter map : (ascii → ascii) → bytes → bytes.
Parameter mapi : (int → ascii → ascii) → bytes → bytes.
Parameter trim : bytes → bytes.
Parameter escaped : bytes → bytes.
Parameter index_opt : bytes → ascii → option int.
Parameter rindex_opt : bytes → ascii → option int.
Parameter index_from_opt : bytes → int → ascii → option int.
Parameter rindex_from_opt : bytes → int → ascii → option int.
Parameter contains : bytes → ascii → bool.
Parameter contains_from : bytes → int → ascii → bool.
Parameter rcontains_from : bytes → int → ascii → bool.
Parameter uppercase_ascii : bytes → bytes.
Parameter lowercase_ascii : bytes → bytes.
Parameter capitalize_ascii : bytes → bytes.
Parameter uncapitalize_ascii : bytes → bytes.
Definition t : Set := bytes.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Bytes_signature.
Require Export Proto_alpha.Environment.Bytes.
Module Bytes_check : Bytes_signature := Bytes.
Module Type Int32_signature.
Parameter zero : int32.
Parameter one : int32.
Parameter minus_one : int32.
Parameter neg : int32 → int32.
Parameter add : int32 → int32 → int32.
Parameter sub : int32 → int32 → int32.
Parameter mul : int32 → int32 → int32.
Parameter div : int32 → int32 → int32.
Parameter rem : int32 → int32 → int32.
Parameter succ : int32 → int32.
Parameter pred : int32 → int32.
Parameter abs : int32 → int32.
Parameter max_int : int32.
Parameter min_int : int32.
Parameter logand : int32 → int32 → int32.
Parameter logor : int32 → int32 → int32.
Parameter logxor : int32 → int32 → int32.
Parameter lognot : int32 → int32.
Parameter shift_left : int32 → int → int32.
Parameter shift_right : int32 → int → int32.
Parameter shift_right_logical : int32 → int → int32.
Parameter of_int : int → int32.
Parameter to_int : int32 → int.
Parameter of_string_opt : string → option int32.
Parameter to_string : int32 → string.
Definition t : Set := int32.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Int32_signature.
Require Export Proto_alpha.Environment.Int32.
Module Int32_check : Int32_signature := Int32.
Module Type Int64_signature.
Parameter zero : int64.
Parameter one : int64.
Parameter minus_one : int64.
Parameter neg : int64 → int64.
Parameter add : int64 → int64 → int64.
Parameter sub : int64 → int64 → int64.
Parameter mul : int64 → int64 → int64.
Parameter div : int64 → int64 → int64.
Parameter rem : int64 → int64 → int64.
Parameter succ : int64 → int64.
Parameter pred : int64 → int64.
Parameter abs : int64 → int64.
Parameter max_int : int64.
Parameter min_int : int64.
Parameter logand : int64 → int64 → int64.
Parameter logor : int64 → int64 → int64.
Parameter logxor : int64 → int64 → int64.
Parameter lognot : int64 → int64.
Parameter shift_left : int64 → int → int64.
Parameter shift_right : int64 → int → int64.
Parameter shift_right_logical : int64 → int → int64.
Parameter of_int : int → int64.
Parameter to_int : int64 → int.
Parameter of_int32 : int32 → int64.
Parameter to_int32 : int64 → int32.
Parameter of_string_opt : string → option int64.
Parameter to_string : int64 → string.
Definition t : Set := int64.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Int64_signature.
Require Export Proto_alpha.Environment.Int64.
Module Int64_check : Int64_signature := Int64.
Module Type Format_signature.
Parameter formatter : Set.
Parameter pp_open_box : formatter → int → unit.
Parameter pp_close_box : formatter → unit → unit.
Parameter pp_open_hbox : formatter → unit → unit.
Parameter pp_open_vbox : formatter → int → unit.
Parameter pp_open_hvbox : formatter → int → unit.
Parameter pp_open_hovbox : formatter → int → unit.
Parameter pp_print_string : formatter → string → unit.
Parameter pp_print_as : formatter → int → string → unit.
Parameter pp_print_int : formatter → int → unit.
Parameter pp_print_char : formatter → ascii → unit.
Parameter pp_print_bool : formatter → bool → unit.
Parameter pp_print_space : formatter → unit → unit.
Parameter pp_print_cut : formatter → unit → unit.
Parameter pp_print_break : formatter → int → int → unit.
Parameter pp_print_custom_break :
formatter → string × int × string → string × int × string → unit.
Parameter pp_force_newline : formatter → unit → unit.
Parameter pp_print_if_newline : formatter → unit → unit.
Parameter pp_print_flush : formatter → unit → unit.
Parameter pp_print_newline : formatter → unit → unit.
Parameter pp_set_margin : formatter → int → unit.
Parameter pp_get_margin : formatter → unit → int.
Parameter pp_set_max_indent : formatter → int → unit.
Parameter pp_get_max_indent : formatter → unit → int.
Parameter pp_set_max_boxes : formatter → int → unit.
Parameter pp_get_max_boxes : formatter → unit → int.
Parameter pp_over_max_boxes : formatter → unit → bool.
Parameter pp_open_tbox : formatter → unit → unit.
Parameter pp_close_tbox : formatter → unit → unit.
Parameter pp_set_tab : formatter → unit → unit.
Parameter pp_print_tab : formatter → unit → unit.
Parameter pp_print_tbreak : formatter → int → int → unit.
Parameter pp_set_ellipsis_text : formatter → string → unit.
Parameter pp_get_ellipsis_text : formatter → unit → string.
Parameter pp_print_list : ∀ {a : Set},
option (formatter → unit → unit) → (formatter → a → unit) →
formatter → list a → unit.
Parameter pp_print_text : formatter → string → unit.
Parameter pp_print_option : ∀ {a : Set},
option (formatter → unit → unit) → (formatter → a → unit) →
formatter → option a → unit.
Parameter pp_print_result : ∀ {a e : Set},
(formatter → a → unit) → (formatter → e → unit) → formatter →
Pervasives.result a e → unit.
Parameter fprintf : ∀ {a : Set},
formatter → Pervasives.format a formatter unit → a.
Parameter sprintf : ∀ {a : Set}, Pervasives.format a unit string → a.
Parameter asprintf : ∀ {a : Set},
Pervasives.format4 a formatter unit string → a.
Parameter dprintf : ∀ {a : Set},
Pervasives.format4 a formatter unit (formatter → unit) → a.
Parameter ifprintf : ∀ {a : Set},
formatter → Pervasives.format a formatter unit → a.
Parameter kfprintf : ∀ {a b : Set},
(formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.
Parameter kdprintf : ∀ {a b : Set},
((formatter → unit) → a) → Pervasives.format4 b formatter unit a → b.
Parameter ikfprintf : ∀ {a b : Set},
(formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.
Parameter ksprintf : ∀ {a b : Set},
(string → a) → Pervasives.format4 b unit string a → b.
Parameter kasprintf : ∀ {a b : Set},
(string → a) → Pervasives.format4 b formatter unit a → b.
End Format_signature.
Require Export Proto_alpha.Environment.Format.
Module Format_check : Format_signature := Format.
Module Type Logging_signature.
Inductive level : Set :=
| Debug : level
| Info : level
| Notice : level
| Warning : level
| Error : level
| Fatal : level.
Parameter log : ∀ {a : Set},
level → Pervasives.format4 a Format.formatter unit unit → a.
Parameter log_string : level → string → unit.
End Logging_signature.
Require Export Proto_alpha.Environment.Logging.
Module Logging_check : Logging_signature := Logging.
Module Type Hex_signature.
Inductive t : Set :=
| Hex : string → t.
Parameter of_char : ascii → ascii × ascii.
Parameter to_char : ascii → ascii → option ascii.
Parameter of_string : option (list ascii) → string → t.
Parameter to_string : t → option string.
Parameter of_bytes : option (list ascii) → bytes → t.
Parameter to_bytes : t → option bytes.
Parameter hexdump_s : option bool → option bool → t → string.
Parameter pp : Format.formatter → t → unit.
Parameter show : t → string.
End Hex_signature.
Require Export Proto_alpha.Environment.Hex.
Module Hex_check : Hex_signature := Hex.
Module Type Z_signature.
Parameter t : Set.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
Parameter of_int : int → t.
Parameter of_int32 : int32 → t.
Parameter of_int64 : int64 → t.
Parameter of_string : string → t.
Parameter of_substring : string → int → int → t.
Parameter of_string_base : int → string → t.
Parameter of_substring_base : int → string → int → int → t.
Parameter succ : t → t.
Parameter pred : t → t.
Parameter abs : t → t.
Parameter neg : t → t.
Parameter add : t → t → t.
Parameter sub : t → t → t.
Parameter mul : t → t → t.
Parameter div : t → t → t.
Parameter rem : t → t → t.
Parameter div_rem : t → t → t × t.
Parameter cdiv : t → t → t.
Parameter fdiv : t → t → t.
Parameter ediv_rem : t → t → t × t.
Parameter ediv : t → t → t.
Parameter erem : t → t → t.
Parameter divexact : t → t → t.
Parameter divisible : t → t → bool.
Parameter congruent : t → t → t → bool.
Parameter logand : t → t → t.
Parameter logor : t → t → t.
Parameter logxor : t → t → t.
Parameter lognot : t → t.
Parameter shift_left : t → int → t.
Parameter shift_right : t → int → t.
Parameter shift_right_trunc : t → int → t.
Parameter numbits : t → int.
Parameter trailing_zeros : t → int.
Parameter testbit : t → int → bool.
Parameter popcount : t → int.
Parameter hamdist : t → t → int.
Parameter to_int : t → int.
Parameter to_int32 : t → int32.
Parameter to_int64 : t → int64.
Parameter to_string : t → string.
Parameter format : string → t → string.
Parameter fits_int : t → bool.
Parameter fits_int32 : t → bool.
Parameter fits_int64 : t → bool.
Parameter pp_print : Format.formatter → t → unit.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter leq : t → t → bool.
Parameter geq : t → t → bool.
Parameter lt : t → t → bool.
Parameter gt : t → t → bool.
Parameter sign : t → int.
Parameter min : t → t → t.
Parameter max : t → t → t.
Parameter is_even : t → bool.
Parameter is_odd : t → bool.
Parameter pow : t → int → t.
Parameter sqrt : t → t.
Parameter sqrt_rem : t → t × t.
Parameter root_value : t → int → t.
Parameter rootrem : t → int → t × t.
Parameter perfect_power : t → bool.
Parameter perfect_square : t → bool.
Parameter log2 : t → int.
Parameter log2up : t → int.
Parameter size_value : t → int.
Parameter extract : t → int → int → t.
Parameter signed_extract : t → int → int → t.
Parameter to_bits : t → string.
Parameter of_bits : string → t.
End Z_signature.
Require Export Proto_alpha.Environment.Z.
Module Z_check : Z_signature := Z.
Module Type Lwt_signature.
Parameter t : ∀ (a : Set), Set.
Parameter _return : ∀ {a : Set}, a → t a.
Parameter bind : ∀ {a b : Set}, t a → (a → t b) → t b.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter return_unit : t unit.
Parameter return_none : ∀ {A : Set}, t (option A).
Parameter return_nil : ∀ {A : Set}, t (list A).
Parameter return_true : t bool.
Parameter return_false : t bool.
End Lwt_signature.
(* We do not implement the Lwt module, as it is the identity monad for us since
the protocol code is sequential and interactions with the store can be
implemented in a purely functional way. *)
Module Type Data_encoding_signature.
Inductive json : Set :=
| Bool : bool → json
| Null : json
| O : list (string × json) → json
| Float : float → json
| String : string → json
| A : list json → json.
Inductive tag_size : Set :=
| Uint16 : tag_size
| Uint8 : tag_size.
Parameter json_schema : Set.
Parameter t : ∀ (a : Set), Set.
Definition encoding (a : Set) : Set := t a.
Parameter classify : ∀ {a : Set}, encoding a → Variant.t.
Parameter null : encoding unit.
Parameter empty : encoding unit.
Parameter unit_value : encoding unit.
Parameter constant : string → encoding unit.
Parameter int8 : encoding int.
Parameter uint8 : encoding int.
Parameter int16 : encoding int.
Parameter uint16 : encoding int.
Parameter int31 : encoding int.
Parameter int32_value : encoding int32.
Parameter int64_value : encoding int64.
Parameter ranged_int : int → int → encoding int.
Parameter z_value : encoding Z.t.
Parameter n_value : encoding Z.t.
Parameter bool_value : encoding bool.
Parameter string_value : encoding string.
Parameter bytes_value : encoding Bytes.t.
Parameter option_value : ∀ {a : Set}, encoding a → encoding (option a).
Parameter result_value : ∀ {a b : Set},
encoding a → encoding b → encoding (Pervasives.result a b).
Parameter array_value : ∀ {a : Set},
option int → encoding a → encoding (array a).
Parameter list_value : ∀ {a : Set},
option int → encoding a → encoding (list a).
Parameter conv : ∀ {a b : Set},
(a → b) → (b → a) → option json_schema → encoding b → encoding a.
Parameter conv_with_guard : ∀ {a b : Set},
(a → b) → (b → Pervasives.result a string) → option json_schema →
encoding b → encoding a.
Parameter with_decoding_guard : ∀ {a : Set},
(a → Pervasives.result unit string) → encoding a → encoding a.
Parameter assoc : ∀ {a : Set},
encoding a → encoding (list (string × a)).
Parameter field : ∀ (a : Set), Set.
Parameter req : ∀ {t : Set},
option string → option string → string → encoding t → field t.
Parameter opt : ∀ {t : Set},
option string → option string → string → encoding t → field (option t).
Parameter varopt : ∀ {t : Set},
option string → option string → string → encoding t → field (option t).
Parameter dft : ∀ {t : Set},
option string → option string → string → encoding t → t → field t.
Parameter obj1 : ∀ {f1 : Set}, field f1 → encoding f1.
Parameter obj2 : ∀ {f1 f2 : Set},
field f1 → field f2 → encoding (f1 × f2).
Parameter obj3 : ∀ {f1 f2 f3 : Set},
field f1 → field f2 → field f3 → encoding (f1 × f2 × f3).
Parameter obj4 : ∀ {f1 f2 f3 f4 : Set},
field f1 → field f2 → field f3 → field f4 → encoding (f1 × f2 × f3 × f4).
Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 →
encoding (f1 × f2 × f3 × f4 × f5).
Parameter obj6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
encoding (f1 × f2 × f3 × f4 × f5 × f6).
Parameter obj7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter obj8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter obj9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter obj10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 → field f10 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter merge_objs : ∀ {o1 o2 : Set},
encoding o1 → encoding o2 → encoding (o1 × o2).
Parameter tup1 : ∀ {f1 : Set}, encoding f1 → encoding f1.
Parameter tup2 : ∀ {f1 f2 : Set},
encoding f1 → encoding f2 → encoding (f1 × f2).
Parameter tup3 : ∀ {f1 f2 f3 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding (f1 × f2 × f3).
Parameter tup4 : ∀ {f1 f2 f3 f4 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 →
encoding (f1 × f2 × f3 × f4).
Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding (f1 × f2 × f3 × f4 × f5).
Parameter tup6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding (f1 × f2 × f3 × f4 × f5 × f6).
Parameter tup7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter tup8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter tup9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 → encoding f9 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter tup10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 → encoding f9 → encoding f10 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter merge_tups : ∀ {a1 a2 : Set},
encoding a1 → encoding a2 → encoding (a1 × a2).
Parameter case : ∀ (t : Set), Set.
Inductive case_tag : Set :=
| Tag : int → case_tag
| Json_only : case_tag.
Parameter match_result : Set.
Definition matching_function (a : Set) : Set := a → match_result.
Parameter matched : ∀ {a : Set},
option Variant.t → int → encoding a → a → match_result.
Parameter case_value : ∀ {a t : Set},
string → option string → case_tag → encoding a → (t → option a) →
(a → t) → case t.
Parameter matching : ∀ {t : Set},
option Variant.t → matching_function t → list (case t) → encoding t.
Parameter union : ∀ {t : Set},
option Variant.t → list (case t) → encoding t.
Parameter string_enum : ∀ {a : Set}, list (string × a) → encoding a.
Module Fixed.
Parameter string_value : int → encoding string.
Parameter bytes_value : int → encoding bytes.
Parameter add_padding : ∀ {a : Set}, encoding a → int → encoding a.
Parameter list_value : ∀ {a : Set},
int → encoding a → encoding (list a).
Parameter array_value : ∀ {a : Set},
int → encoding a → encoding (array a).
End Fixed.
Module _Variable.
Parameter string_value : encoding string.
Parameter bytes_value : encoding bytes.
Parameter array_value : ∀ {a : Set},
option int → encoding a → encoding (array a).
Parameter list_value : ∀ {a : Set},
option int → encoding a → encoding (list a).
End _Variable.
Module Bounded.
Parameter string_value : int → encoding string.
Parameter bytes_value : int → encoding bytes.
End Bounded.
Parameter dynamic_size : ∀ {a : Set},
option Variant.t → encoding a → encoding a.
Parameter check_size : ∀ {a : Set}, int → encoding a → encoding a.
Parameter splitted : ∀ {a : Set}, encoding a → encoding a → encoding a.
Parameter mu : ∀ {a : Set},
string → option string → option string → (encoding a → encoding a) →
encoding a.
Parameter def : ∀ {t : Set},
string → option string → option string → encoding t → encoding t.
Parameter lazy_t : ∀ (a : Set), Set.
Parameter lazy_encoding : ∀ {a : Set}, encoding a → encoding (lazy_t a).
Parameter force_decode : ∀ {a : Set}, lazy_t a → option a.
Parameter force_bytes : ∀ {a : Set}, lazy_t a → bytes.
Parameter make_lazy : ∀ {a : Set}, encoding a → a → lazy_t a.
Parameter apply_lazy : ∀ {a b : Set},
(a → b) → (bytes → b) → (b → b → b) → lazy_t a → b.
Module Compact.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, option Variant.t → t a → encoding a.
Parameter tag_bit_count : ∀ {a : Set}, t a → int.
Parameter void : Set.
Parameter void_value : t void.
Parameter refute : ∀ {a : Set}, void → a.
Parameter unit_value : t unit.
Parameter bool_value : t bool.
Parameter payload : ∀ {a : Set}, encoding a → t a.
Parameter option_value : ∀ {a : Set}, t a → t (option a).
Parameter conv : ∀ {a b : Set},
option (encoding a) → (a → b) → (b → a) → t b → t a.
Parameter tup1 : ∀ {a : Set}, t a → t a.
Parameter tup2 : ∀ {a b : Set}, t a → t b → t (a × b).
Parameter tup3 : ∀ {a b c : Set}, t a → t b → t c → t (a × b × c).
Parameter tup4 : ∀ {a b c d : Set},
t a → t b → t c → t d → t (a × b × c × d).
Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t (f1 × f2 × f3 × f4 × f5).
Parameter tup6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 →
t (f1 × f2 × f3 × f4 × f5 × f6).
Parameter tup7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter tup8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter tup9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter tup10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
t f10 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter field : ∀ (a : Set), Set.
Parameter req : ∀ {a : Set}, string → t a → field a.
Parameter opt : ∀ {a : Set}, string → t a → field (option a).
Parameter obj1 : ∀ {a : Set}, field a → t a.
Parameter obj2 : ∀ {a b : Set}, field a → field b → t (a × b).
Parameter obj3 : ∀ {a b c : Set},
field a → field b → field c → t (a × b × c).
Parameter obj4 : ∀ {a b c d : Set},
field a → field b → field c → field d → t (a × b × c × d).
Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 →
t (f1 × f2 × f3 × f4 × f5).
Parameter obj6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
t (f1 × f2 × f3 × f4 × f5 × f6).
Parameter obj7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter obj8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter obj9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter obj10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 → field f10 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter int32_value : t int32.
Parameter int64_value : t int64.
Parameter list_value : ∀ {a : Set}, int → encoding a → t (list a).
Parameter case : ∀ (a : Set), Set.
Parameter case_value : ∀ {a b : Set},
string → option string → t b → (a → option b) → (b → a) → case a.
Parameter union : ∀ {a : Set},
option int → option int → list (case a) → t a.
Parameter void_case : ∀ {a : Set}, string → case a.
Parameter or_int32 : ∀ {a : Set},
string → string → option string → encoding a → t (Either.t int32 a).
Module Custom.
Definition tag : Set := int.
Parameter join_tags : list (tag × int) → tag.
Module S.
Record signature {input layout : Set} : Set := {
Require Import CoqOfOCaml.Settings.
Require Import Proto_alpha.Environment.Variant.
Module Type Pervasives_signature.
Parameter raise : ∀ {a : Set}, extensible_type → a.
Parameter raise_notrace : ∀ {a : Set}, extensible_type → a.
Parameter invalid_arg : ∀ {a : Set}, string → a.
Parameter failwith : ∀ {a : Set}, string → a.
Parameter not : bool → bool.
Parameter op_andand : bool → bool → bool.
Parameter op_pipepipe : bool → bool → bool.
Parameter __LOC__ : string.
Parameter __FILE__ : string.
Parameter __LINE__ : int.
Parameter __MODULE__ : string.
Parameter __POS__ : string × int × int × int.
Parameter __LOC_OF__ : ∀ {a : Set}, a → string × a.
Parameter __LINE_OF__ : ∀ {a : Set}, a → int × a.
Parameter __POS_OF__ : ∀ {a : Set}, a → (string × int × int × int) × a.
Parameter op_pipegt : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_atat : ∀ {a b : Set}, (a → b) → a → b.
Parameter op_tildeminus : int → int.
Parameter op_tildeplus : int → int.
Parameter succ : int → int.
Parameter pred : int → int.
Parameter op_plus : int → int → int.
Parameter op_minus : int → int → int.
Parameter op_star : int → int → int.
Parameter op_div : int → int → int.
Parameter _mod : int → int → int.
Parameter abs : int → int.
Parameter max_int : int.
Parameter min_int : int.
Parameter land : int → int → int.
Parameter lor : int → int → int.
Parameter lxor : int → int → int.
Parameter lnot : int → int.
Parameter lsl : int → int → int.
Parameter lsr : int → int → int.
Parameter asr : int → int → int.
Parameter op_caret : string → string → string.
Parameter int_of_char : ascii → int.
Parameter char_of_int : int → ascii.
Parameter ignore : ∀ {a : Set}, a → unit.
Parameter string_of_bool : bool → string.
Parameter bool_of_string_opt : string → option bool.
Parameter string_of_int : int → string.
Parameter int_of_string_opt : string → option int.
Parameter fst : ∀ {a b : Set}, a × b → a.
Parameter snd : ∀ {a b : Set}, a × b → b.
Parameter op_at : ∀ {a : Set}, list a → list a → list a.
Module ref.
Record record {a : Set} : Set := Build {
contents : a;
}.
Arguments record : clear implicits.
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a contents.
End ref.
Definition ref := ref.record.
Parameter ref_value : ∀ {a : Set}, a → ref a.
Parameter op_exclamation : ∀ {a : Set}, ref a → a.
Parameter op_coloneq : ∀ {a : Set}, ref a → a → unit.
Parameter incr : ref int → unit.
Parameter decr : ref int → unit.
Inductive result (a b : Set) : Set :=
| Ok : a → result a b
| Error : b → result a b.
Arguments Ok {_ _}.
Arguments Error {_ _}.
Definition format6 (a b c d e f : Set) : Set :=
CamlinternalFormatBasics.format6 a b c d e f.
Definition format4 (a b c d : Set) : Set := format6 a b c c c d.
Definition format (a b c : Set) : Set := format4 a b c c.
Parameter string_of_format : ∀ {a b c d e f : Set},
format6 a b c d e f → string.
Parameter format_of_string : ∀ {a b c d e f : Set},
format6 a b c d e f → format6 a b c d e f.
Parameter op_caretcaret : ∀ {a b c d e f g h : Set},
format6 a b c d e f → format6 f b c e g h → format6 a b c d g h.
End Pervasives_signature.
Require Export Proto_alpha.Environment.Pervasives.
Module Pervasives_check : Pervasives_signature := Pervasives.
Module Type Either_signature.
Inductive t (a b : Set) : Set :=
| Left : a → t a b
| Right : b → t a b.
Arguments Left {_ _}.
Arguments Right {_ _}.
Parameter equal : ∀ {a b : Set},
(a → a → bool) → (b → b → bool) → t a b → t a b → bool.
Parameter compare : ∀ {a b : Set},
(a → a → int) → (b → b → int) → t a b → t a b → int.
End Either_signature.
Require Export Proto_alpha.Environment.Either.
Module Either_check : Either_signature := Either.
Module Type String_signature.
Parameter length : string → int.
Parameter get : string → int → ascii.
Parameter make : int → ascii → string.
Parameter init_value : int → (int → ascii) → string.
Parameter sub : string → int → int → string.
Parameter blit : string → int → bytes → int → int → unit.
Parameter concat : string → list string → string.
Parameter iter : (ascii → unit) → string → unit.
Parameter iteri : (int → ascii → unit) → string → unit.
Parameter map : (ascii → ascii) → string → string.
Parameter mapi : (int → ascii → ascii) → string → string.
Parameter trim : string → string.
Parameter escaped : string → string.
Parameter index_opt : string → ascii → option int.
Parameter rindex_opt : string → ascii → option int.
Parameter index_from_opt : string → int → ascii → option int.
Parameter rindex_from_opt : string → int → ascii → option int.
Parameter contains : string → ascii → bool.
Parameter contains_from : string → int → ascii → bool.
Parameter rcontains_from : string → int → ascii → bool.
Parameter uppercase_ascii : string → string.
Parameter lowercase_ascii : string → string.
Parameter capitalize_ascii : string → string.
Parameter uncapitalize_ascii : string → string.
Definition t : Set := string.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter split_on_char : ascii → string → list string.
End String_signature.
Require Export Proto_alpha.Environment.String.
Module String_check : String_signature := String.
Module Type Char_signature.
Parameter code : ascii → int.
Parameter chr : int → ascii.
Parameter escaped : ascii → string.
Parameter lowercase_ascii : ascii → ascii.
Parameter uppercase_ascii : ascii → ascii.
Definition t : Set := ascii.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Char_signature.
Require Export Proto_alpha.Environment.Char.
Module Char_check : Char_signature := Char.
Module Type Bytes_signature.
Parameter length : bytes → int.
Parameter get : bytes → int → ascii.
Parameter set : bytes → int → ascii → unit.
Parameter make : int → ascii → bytes.
Parameter init_value : int → (int → ascii) → bytes.
Parameter empty : bytes.
Parameter copy : bytes → bytes.
Parameter of_string : string → bytes.
Parameter to_string : bytes → string.
Parameter sub : bytes → int → int → bytes.
Parameter sub_string : bytes → int → int → string.
Parameter extend : bytes → int → int → bytes.
Parameter fill : bytes → int → int → ascii → unit.
Parameter blit : bytes → int → bytes → int → int → unit.
Parameter blit_string : string → int → bytes → int → int → unit.
Parameter concat : bytes → list bytes → bytes.
Parameter cat : bytes → bytes → bytes.
Parameter iter : (ascii → unit) → bytes → unit.
Parameter iteri : (int → ascii → unit) → bytes → unit.
Parameter map : (ascii → ascii) → bytes → bytes.
Parameter mapi : (int → ascii → ascii) → bytes → bytes.
Parameter trim : bytes → bytes.
Parameter escaped : bytes → bytes.
Parameter index_opt : bytes → ascii → option int.
Parameter rindex_opt : bytes → ascii → option int.
Parameter index_from_opt : bytes → int → ascii → option int.
Parameter rindex_from_opt : bytes → int → ascii → option int.
Parameter contains : bytes → ascii → bool.
Parameter contains_from : bytes → int → ascii → bool.
Parameter rcontains_from : bytes → int → ascii → bool.
Parameter uppercase_ascii : bytes → bytes.
Parameter lowercase_ascii : bytes → bytes.
Parameter capitalize_ascii : bytes → bytes.
Parameter uncapitalize_ascii : bytes → bytes.
Definition t : Set := bytes.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Bytes_signature.
Require Export Proto_alpha.Environment.Bytes.
Module Bytes_check : Bytes_signature := Bytes.
Module Type Int32_signature.
Parameter zero : int32.
Parameter one : int32.
Parameter minus_one : int32.
Parameter neg : int32 → int32.
Parameter add : int32 → int32 → int32.
Parameter sub : int32 → int32 → int32.
Parameter mul : int32 → int32 → int32.
Parameter div : int32 → int32 → int32.
Parameter rem : int32 → int32 → int32.
Parameter succ : int32 → int32.
Parameter pred : int32 → int32.
Parameter abs : int32 → int32.
Parameter max_int : int32.
Parameter min_int : int32.
Parameter logand : int32 → int32 → int32.
Parameter logor : int32 → int32 → int32.
Parameter logxor : int32 → int32 → int32.
Parameter lognot : int32 → int32.
Parameter shift_left : int32 → int → int32.
Parameter shift_right : int32 → int → int32.
Parameter shift_right_logical : int32 → int → int32.
Parameter of_int : int → int32.
Parameter to_int : int32 → int.
Parameter of_string_opt : string → option int32.
Parameter to_string : int32 → string.
Definition t : Set := int32.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Int32_signature.
Require Export Proto_alpha.Environment.Int32.
Module Int32_check : Int32_signature := Int32.
Module Type Int64_signature.
Parameter zero : int64.
Parameter one : int64.
Parameter minus_one : int64.
Parameter neg : int64 → int64.
Parameter add : int64 → int64 → int64.
Parameter sub : int64 → int64 → int64.
Parameter mul : int64 → int64 → int64.
Parameter div : int64 → int64 → int64.
Parameter rem : int64 → int64 → int64.
Parameter succ : int64 → int64.
Parameter pred : int64 → int64.
Parameter abs : int64 → int64.
Parameter max_int : int64.
Parameter min_int : int64.
Parameter logand : int64 → int64 → int64.
Parameter logor : int64 → int64 → int64.
Parameter logxor : int64 → int64 → int64.
Parameter lognot : int64 → int64.
Parameter shift_left : int64 → int → int64.
Parameter shift_right : int64 → int → int64.
Parameter shift_right_logical : int64 → int → int64.
Parameter of_int : int → int64.
Parameter to_int : int64 → int.
Parameter of_int32 : int32 → int64.
Parameter to_int32 : int64 → int32.
Parameter of_string_opt : string → option int64.
Parameter to_string : int64 → string.
Definition t : Set := int64.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
End Int64_signature.
Require Export Proto_alpha.Environment.Int64.
Module Int64_check : Int64_signature := Int64.
Module Type Format_signature.
Parameter formatter : Set.
Parameter pp_open_box : formatter → int → unit.
Parameter pp_close_box : formatter → unit → unit.
Parameter pp_open_hbox : formatter → unit → unit.
Parameter pp_open_vbox : formatter → int → unit.
Parameter pp_open_hvbox : formatter → int → unit.
Parameter pp_open_hovbox : formatter → int → unit.
Parameter pp_print_string : formatter → string → unit.
Parameter pp_print_as : formatter → int → string → unit.
Parameter pp_print_int : formatter → int → unit.
Parameter pp_print_char : formatter → ascii → unit.
Parameter pp_print_bool : formatter → bool → unit.
Parameter pp_print_space : formatter → unit → unit.
Parameter pp_print_cut : formatter → unit → unit.
Parameter pp_print_break : formatter → int → int → unit.
Parameter pp_print_custom_break :
formatter → string × int × string → string × int × string → unit.
Parameter pp_force_newline : formatter → unit → unit.
Parameter pp_print_if_newline : formatter → unit → unit.
Parameter pp_print_flush : formatter → unit → unit.
Parameter pp_print_newline : formatter → unit → unit.
Parameter pp_set_margin : formatter → int → unit.
Parameter pp_get_margin : formatter → unit → int.
Parameter pp_set_max_indent : formatter → int → unit.
Parameter pp_get_max_indent : formatter → unit → int.
Parameter pp_set_max_boxes : formatter → int → unit.
Parameter pp_get_max_boxes : formatter → unit → int.
Parameter pp_over_max_boxes : formatter → unit → bool.
Parameter pp_open_tbox : formatter → unit → unit.
Parameter pp_close_tbox : formatter → unit → unit.
Parameter pp_set_tab : formatter → unit → unit.
Parameter pp_print_tab : formatter → unit → unit.
Parameter pp_print_tbreak : formatter → int → int → unit.
Parameter pp_set_ellipsis_text : formatter → string → unit.
Parameter pp_get_ellipsis_text : formatter → unit → string.
Parameter pp_print_list : ∀ {a : Set},
option (formatter → unit → unit) → (formatter → a → unit) →
formatter → list a → unit.
Parameter pp_print_text : formatter → string → unit.
Parameter pp_print_option : ∀ {a : Set},
option (formatter → unit → unit) → (formatter → a → unit) →
formatter → option a → unit.
Parameter pp_print_result : ∀ {a e : Set},
(formatter → a → unit) → (formatter → e → unit) → formatter →
Pervasives.result a e → unit.
Parameter fprintf : ∀ {a : Set},
formatter → Pervasives.format a formatter unit → a.
Parameter sprintf : ∀ {a : Set}, Pervasives.format a unit string → a.
Parameter asprintf : ∀ {a : Set},
Pervasives.format4 a formatter unit string → a.
Parameter dprintf : ∀ {a : Set},
Pervasives.format4 a formatter unit (formatter → unit) → a.
Parameter ifprintf : ∀ {a : Set},
formatter → Pervasives.format a formatter unit → a.
Parameter kfprintf : ∀ {a b : Set},
(formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.
Parameter kdprintf : ∀ {a b : Set},
((formatter → unit) → a) → Pervasives.format4 b formatter unit a → b.
Parameter ikfprintf : ∀ {a b : Set},
(formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.
Parameter ksprintf : ∀ {a b : Set},
(string → a) → Pervasives.format4 b unit string a → b.
Parameter kasprintf : ∀ {a b : Set},
(string → a) → Pervasives.format4 b formatter unit a → b.
End Format_signature.
Require Export Proto_alpha.Environment.Format.
Module Format_check : Format_signature := Format.
Module Type Logging_signature.
Inductive level : Set :=
| Debug : level
| Info : level
| Notice : level
| Warning : level
| Error : level
| Fatal : level.
Parameter log : ∀ {a : Set},
level → Pervasives.format4 a Format.formatter unit unit → a.
Parameter log_string : level → string → unit.
End Logging_signature.
Require Export Proto_alpha.Environment.Logging.
Module Logging_check : Logging_signature := Logging.
Module Type Hex_signature.
Inductive t : Set :=
| Hex : string → t.
Parameter of_char : ascii → ascii × ascii.
Parameter to_char : ascii → ascii → option ascii.
Parameter of_string : option (list ascii) → string → t.
Parameter to_string : t → option string.
Parameter of_bytes : option (list ascii) → bytes → t.
Parameter to_bytes : t → option bytes.
Parameter hexdump_s : option bool → option bool → t → string.
Parameter pp : Format.formatter → t → unit.
Parameter show : t → string.
End Hex_signature.
Require Export Proto_alpha.Environment.Hex.
Module Hex_check : Hex_signature := Hex.
Module Type Z_signature.
Parameter t : Set.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
Parameter of_int : int → t.
Parameter of_int32 : int32 → t.
Parameter of_int64 : int64 → t.
Parameter of_string : string → t.
Parameter of_substring : string → int → int → t.
Parameter of_string_base : int → string → t.
Parameter of_substring_base : int → string → int → int → t.
Parameter succ : t → t.
Parameter pred : t → t.
Parameter abs : t → t.
Parameter neg : t → t.
Parameter add : t → t → t.
Parameter sub : t → t → t.
Parameter mul : t → t → t.
Parameter div : t → t → t.
Parameter rem : t → t → t.
Parameter div_rem : t → t → t × t.
Parameter cdiv : t → t → t.
Parameter fdiv : t → t → t.
Parameter ediv_rem : t → t → t × t.
Parameter ediv : t → t → t.
Parameter erem : t → t → t.
Parameter divexact : t → t → t.
Parameter divisible : t → t → bool.
Parameter congruent : t → t → t → bool.
Parameter logand : t → t → t.
Parameter logor : t → t → t.
Parameter logxor : t → t → t.
Parameter lognot : t → t.
Parameter shift_left : t → int → t.
Parameter shift_right : t → int → t.
Parameter shift_right_trunc : t → int → t.
Parameter numbits : t → int.
Parameter trailing_zeros : t → int.
Parameter testbit : t → int → bool.
Parameter popcount : t → int.
Parameter hamdist : t → t → int.
Parameter to_int : t → int.
Parameter to_int32 : t → int32.
Parameter to_int64 : t → int64.
Parameter to_string : t → string.
Parameter format : string → t → string.
Parameter fits_int : t → bool.
Parameter fits_int32 : t → bool.
Parameter fits_int64 : t → bool.
Parameter pp_print : Format.formatter → t → unit.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter leq : t → t → bool.
Parameter geq : t → t → bool.
Parameter lt : t → t → bool.
Parameter gt : t → t → bool.
Parameter sign : t → int.
Parameter min : t → t → t.
Parameter max : t → t → t.
Parameter is_even : t → bool.
Parameter is_odd : t → bool.
Parameter pow : t → int → t.
Parameter sqrt : t → t.
Parameter sqrt_rem : t → t × t.
Parameter root_value : t → int → t.
Parameter rootrem : t → int → t × t.
Parameter perfect_power : t → bool.
Parameter perfect_square : t → bool.
Parameter log2 : t → int.
Parameter log2up : t → int.
Parameter size_value : t → int.
Parameter extract : t → int → int → t.
Parameter signed_extract : t → int → int → t.
Parameter to_bits : t → string.
Parameter of_bits : string → t.
End Z_signature.
Require Export Proto_alpha.Environment.Z.
Module Z_check : Z_signature := Z.
Module Type Lwt_signature.
Parameter t : ∀ (a : Set), Set.
Parameter _return : ∀ {a : Set}, a → t a.
Parameter bind : ∀ {a b : Set}, t a → (a → t b) → t b.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter return_unit : t unit.
Parameter return_none : ∀ {A : Set}, t (option A).
Parameter return_nil : ∀ {A : Set}, t (list A).
Parameter return_true : t bool.
Parameter return_false : t bool.
End Lwt_signature.
(* We do not implement the Lwt module, as it is the identity monad for us since
the protocol code is sequential and interactions with the store can be
implemented in a purely functional way. *)
Module Type Data_encoding_signature.
Inductive json : Set :=
| Bool : bool → json
| Null : json
| O : list (string × json) → json
| Float : float → json
| String : string → json
| A : list json → json.
Inductive tag_size : Set :=
| Uint16 : tag_size
| Uint8 : tag_size.
Parameter json_schema : Set.
Parameter t : ∀ (a : Set), Set.
Definition encoding (a : Set) : Set := t a.
Parameter classify : ∀ {a : Set}, encoding a → Variant.t.
Parameter null : encoding unit.
Parameter empty : encoding unit.
Parameter unit_value : encoding unit.
Parameter constant : string → encoding unit.
Parameter int8 : encoding int.
Parameter uint8 : encoding int.
Parameter int16 : encoding int.
Parameter uint16 : encoding int.
Parameter int31 : encoding int.
Parameter int32_value : encoding int32.
Parameter int64_value : encoding int64.
Parameter ranged_int : int → int → encoding int.
Parameter z_value : encoding Z.t.
Parameter n_value : encoding Z.t.
Parameter bool_value : encoding bool.
Parameter string_value : encoding string.
Parameter bytes_value : encoding Bytes.t.
Parameter option_value : ∀ {a : Set}, encoding a → encoding (option a).
Parameter result_value : ∀ {a b : Set},
encoding a → encoding b → encoding (Pervasives.result a b).
Parameter array_value : ∀ {a : Set},
option int → encoding a → encoding (array a).
Parameter list_value : ∀ {a : Set},
option int → encoding a → encoding (list a).
Parameter conv : ∀ {a b : Set},
(a → b) → (b → a) → option json_schema → encoding b → encoding a.
Parameter conv_with_guard : ∀ {a b : Set},
(a → b) → (b → Pervasives.result a string) → option json_schema →
encoding b → encoding a.
Parameter with_decoding_guard : ∀ {a : Set},
(a → Pervasives.result unit string) → encoding a → encoding a.
Parameter assoc : ∀ {a : Set},
encoding a → encoding (list (string × a)).
Parameter field : ∀ (a : Set), Set.
Parameter req : ∀ {t : Set},
option string → option string → string → encoding t → field t.
Parameter opt : ∀ {t : Set},
option string → option string → string → encoding t → field (option t).
Parameter varopt : ∀ {t : Set},
option string → option string → string → encoding t → field (option t).
Parameter dft : ∀ {t : Set},
option string → option string → string → encoding t → t → field t.
Parameter obj1 : ∀ {f1 : Set}, field f1 → encoding f1.
Parameter obj2 : ∀ {f1 f2 : Set},
field f1 → field f2 → encoding (f1 × f2).
Parameter obj3 : ∀ {f1 f2 f3 : Set},
field f1 → field f2 → field f3 → encoding (f1 × f2 × f3).
Parameter obj4 : ∀ {f1 f2 f3 f4 : Set},
field f1 → field f2 → field f3 → field f4 → encoding (f1 × f2 × f3 × f4).
Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 →
encoding (f1 × f2 × f3 × f4 × f5).
Parameter obj6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
encoding (f1 × f2 × f3 × f4 × f5 × f6).
Parameter obj7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter obj8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter obj9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter obj10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 → field f10 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter merge_objs : ∀ {o1 o2 : Set},
encoding o1 → encoding o2 → encoding (o1 × o2).
Parameter tup1 : ∀ {f1 : Set}, encoding f1 → encoding f1.
Parameter tup2 : ∀ {f1 f2 : Set},
encoding f1 → encoding f2 → encoding (f1 × f2).
Parameter tup3 : ∀ {f1 f2 f3 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding (f1 × f2 × f3).
Parameter tup4 : ∀ {f1 f2 f3 f4 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 →
encoding (f1 × f2 × f3 × f4).
Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding (f1 × f2 × f3 × f4 × f5).
Parameter tup6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding (f1 × f2 × f3 × f4 × f5 × f6).
Parameter tup7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter tup8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter tup9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 → encoding f9 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter tup10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
encoding f6 → encoding f7 → encoding f8 → encoding f9 → encoding f10 →
encoding (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter merge_tups : ∀ {a1 a2 : Set},
encoding a1 → encoding a2 → encoding (a1 × a2).
Parameter case : ∀ (t : Set), Set.
Inductive case_tag : Set :=
| Tag : int → case_tag
| Json_only : case_tag.
Parameter match_result : Set.
Definition matching_function (a : Set) : Set := a → match_result.
Parameter matched : ∀ {a : Set},
option Variant.t → int → encoding a → a → match_result.
Parameter case_value : ∀ {a t : Set},
string → option string → case_tag → encoding a → (t → option a) →
(a → t) → case t.
Parameter matching : ∀ {t : Set},
option Variant.t → matching_function t → list (case t) → encoding t.
Parameter union : ∀ {t : Set},
option Variant.t → list (case t) → encoding t.
Parameter string_enum : ∀ {a : Set}, list (string × a) → encoding a.
Module Fixed.
Parameter string_value : int → encoding string.
Parameter bytes_value : int → encoding bytes.
Parameter add_padding : ∀ {a : Set}, encoding a → int → encoding a.
Parameter list_value : ∀ {a : Set},
int → encoding a → encoding (list a).
Parameter array_value : ∀ {a : Set},
int → encoding a → encoding (array a).
End Fixed.
Module _Variable.
Parameter string_value : encoding string.
Parameter bytes_value : encoding bytes.
Parameter array_value : ∀ {a : Set},
option int → encoding a → encoding (array a).
Parameter list_value : ∀ {a : Set},
option int → encoding a → encoding (list a).
End _Variable.
Module Bounded.
Parameter string_value : int → encoding string.
Parameter bytes_value : int → encoding bytes.
End Bounded.
Parameter dynamic_size : ∀ {a : Set},
option Variant.t → encoding a → encoding a.
Parameter check_size : ∀ {a : Set}, int → encoding a → encoding a.
Parameter splitted : ∀ {a : Set}, encoding a → encoding a → encoding a.
Parameter mu : ∀ {a : Set},
string → option string → option string → (encoding a → encoding a) →
encoding a.
Parameter def : ∀ {t : Set},
string → option string → option string → encoding t → encoding t.
Parameter lazy_t : ∀ (a : Set), Set.
Parameter lazy_encoding : ∀ {a : Set}, encoding a → encoding (lazy_t a).
Parameter force_decode : ∀ {a : Set}, lazy_t a → option a.
Parameter force_bytes : ∀ {a : Set}, lazy_t a → bytes.
Parameter make_lazy : ∀ {a : Set}, encoding a → a → lazy_t a.
Parameter apply_lazy : ∀ {a b : Set},
(a → b) → (bytes → b) → (b → b → b) → lazy_t a → b.
Module Compact.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, option Variant.t → t a → encoding a.
Parameter tag_bit_count : ∀ {a : Set}, t a → int.
Parameter void : Set.
Parameter void_value : t void.
Parameter refute : ∀ {a : Set}, void → a.
Parameter unit_value : t unit.
Parameter bool_value : t bool.
Parameter payload : ∀ {a : Set}, encoding a → t a.
Parameter option_value : ∀ {a : Set}, t a → t (option a).
Parameter conv : ∀ {a b : Set},
option (encoding a) → (a → b) → (b → a) → t b → t a.
Parameter tup1 : ∀ {a : Set}, t a → t a.
Parameter tup2 : ∀ {a b : Set}, t a → t b → t (a × b).
Parameter tup3 : ∀ {a b c : Set}, t a → t b → t c → t (a × b × c).
Parameter tup4 : ∀ {a b c d : Set},
t a → t b → t c → t d → t (a × b × c × d).
Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t (f1 × f2 × f3 × f4 × f5).
Parameter tup6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 →
t (f1 × f2 × f3 × f4 × f5 × f6).
Parameter tup7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter tup8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter tup9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter tup10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
t f10 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter field : ∀ (a : Set), Set.
Parameter req : ∀ {a : Set}, string → t a → field a.
Parameter opt : ∀ {a : Set}, string → t a → field (option a).
Parameter obj1 : ∀ {a : Set}, field a → t a.
Parameter obj2 : ∀ {a b : Set}, field a → field b → t (a × b).
Parameter obj3 : ∀ {a b c : Set},
field a → field b → field c → t (a × b × c).
Parameter obj4 : ∀ {a b c d : Set},
field a → field b → field c → field d → t (a × b × c × d).
Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 →
t (f1 × f2 × f3 × f4 × f5).
Parameter obj6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
t (f1 × f2 × f3 × f4 × f5 × f6).
Parameter obj7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7).
Parameter obj8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).
Parameter obj9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).
Parameter obj10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
field f7 → field f8 → field f9 → field f10 →
t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).
Parameter int32_value : t int32.
Parameter int64_value : t int64.
Parameter list_value : ∀ {a : Set}, int → encoding a → t (list a).
Parameter case : ∀ (a : Set), Set.
Parameter case_value : ∀ {a b : Set},
string → option string → t b → (a → option b) → (b → a) → case a.
Parameter union : ∀ {a : Set},
option int → option int → list (case a) → t a.
Parameter void_case : ∀ {a : Set}, string → case a.
Parameter or_int32 : ∀ {a : Set},
string → string → option string → encoding a → t (Either.t int32 a).
Module Custom.
Definition tag : Set := int.
Parameter join_tags : list (tag × int) → tag.
Module S.
Record signature {input layout : Set} : Set := {
The type of [input] this module allows to encode.
The various ways to efficiently encode [input].
The list of layouts available to encode [input].
The number of bits necessary to distinguish between the various
layouts.
[tag layout] computes the tag of {!Data_encoding.union} to be
used to encode values classified as [layout].
{b Warning:} It is expected that [tag layout < 2^tag_len - 1].
[partial_encoding layout] returns the encoding to use for values
classified as [layout].
This encoding can be partial in the sense that it may fail (it
will raise an [Invalid_argument]) for some values of [x].
However, it is expected that [partial_encoding (classify x) x]
will always succeed.
[classify x] returns the layout to be used to encode [x].
The encoding to use when targeting a JSON output.
json_encoding : encoding input;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Parameter make : ∀ {a : Set},
{layout : Set @ S (input := a) (layout := layout)} → t a.
End Custom.
End Compact.
Definition compact (a : Set) : Set := Compact.t a.
Parameter json_value : encoding json.
Parameter json_schema_value : encoding json_schema.
Module Json.
Parameter schema : ∀ {a : Set},
option string → encoding a → json_schema.
Parameter construct : ∀ {t : Set},
option Variant.t → encoding t → t → json.
Parameter destruct : ∀ {t : Set},
option bool → encoding t → json → t.
Reserved Notation "'path".
Inductive path_item : Set :=
| Index : int → path_item
| Field : string → path_item
| Next : path_item
| Star : path_item
where "'path" := (list path_item).
Definition path := 'path.
Parameter print_error :
option (Format.formatter → extensible_type → unit) →
Format.formatter → extensible_type → unit.
Parameter cannot_destruct : ∀ {a b : Set},
Pervasives.format4 a Format.formatter unit b → a.
Parameter wrap_error : ∀ {a b : Set}, (a → b) → a → b.
Parameter pp : Format.formatter → json → unit.
End Json.
Module Binary.
Parameter length : ∀ {a : Set}, encoding a → a → int.
Parameter fixed_length : ∀ {a : Set}, encoding a → option int.
Parameter maximum_length : ∀ {a : Set}, encoding a → option int.
Parameter of_bytes_opt : ∀ {a : Set}, encoding a → bytes → option a.
Parameter of_string_opt : ∀ {a : Set},
encoding a → string → option a.
Parameter to_bytes_opt : ∀ {a : Set},
option int → encoding a → a → option bytes.
Parameter to_bytes_exn : ∀ {a : Set},
option int → encoding a → a → bytes.
Parameter to_string_opt : ∀ {a : Set},
option int → encoding a → a → option string.
Parameter to_string_exn : ∀ {a : Set},
option int → encoding a → a → string.
End Binary.
End Data_encoding_signature.
Require Export Proto_alpha.Environment.Data_encoding.
Module Data_encoding_check : Data_encoding_signature := Data_encoding.
Module Type Raw_hashes_signature.
Parameter blake2b : bytes → bytes.
Parameter sha256 : bytes → bytes.
Parameter sha512 : bytes → bytes.
Parameter keccak256 : bytes → bytes.
Parameter sha3_256 : bytes → bytes.
Parameter sha3_512 : bytes → bytes.
End Raw_hashes_signature.
Require Export Proto_alpha.Environment.Raw_hashes.
Module Raw_hashes_check : Raw_hashes_signature := Raw_hashes.
Module Type Compare_signature.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S.
Record signature {t : Set} : Set := {
t := t;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Parameter make : ∀ {a : Set},
{layout : Set @ S (input := a) (layout := layout)} → t a.
End Custom.
End Compact.
Definition compact (a : Set) : Set := Compact.t a.
Parameter json_value : encoding json.
Parameter json_schema_value : encoding json_schema.
Module Json.
Parameter schema : ∀ {a : Set},
option string → encoding a → json_schema.
Parameter construct : ∀ {t : Set},
option Variant.t → encoding t → t → json.
Parameter destruct : ∀ {t : Set},
option bool → encoding t → json → t.
Reserved Notation "'path".
Inductive path_item : Set :=
| Index : int → path_item
| Field : string → path_item
| Next : path_item
| Star : path_item
where "'path" := (list path_item).
Definition path := 'path.
Parameter print_error :
option (Format.formatter → extensible_type → unit) →
Format.formatter → extensible_type → unit.
Parameter cannot_destruct : ∀ {a b : Set},
Pervasives.format4 a Format.formatter unit b → a.
Parameter wrap_error : ∀ {a b : Set}, (a → b) → a → b.
Parameter pp : Format.formatter → json → unit.
End Json.
Module Binary.
Parameter length : ∀ {a : Set}, encoding a → a → int.
Parameter fixed_length : ∀ {a : Set}, encoding a → option int.
Parameter maximum_length : ∀ {a : Set}, encoding a → option int.
Parameter of_bytes_opt : ∀ {a : Set}, encoding a → bytes → option a.
Parameter of_string_opt : ∀ {a : Set},
encoding a → string → option a.
Parameter to_bytes_opt : ∀ {a : Set},
option int → encoding a → a → option bytes.
Parameter to_bytes_exn : ∀ {a : Set},
option int → encoding a → a → bytes.
Parameter to_string_opt : ∀ {a : Set},
option int → encoding a → a → option string.
Parameter to_string_exn : ∀ {a : Set},
option int → encoding a → a → string.
End Binary.
End Data_encoding_signature.
Require Export Proto_alpha.Environment.Data_encoding.
Module Data_encoding_check : Data_encoding_signature := Data_encoding.
Module Type Raw_hashes_signature.
Parameter blake2b : bytes → bytes.
Parameter sha256 : bytes → bytes.
Parameter sha512 : bytes → bytes.
Parameter keccak256 : bytes → bytes.
Parameter sha3_256 : bytes → bytes.
Parameter sha3_512 : bytes → bytes.
End Raw_hashes_signature.
Require Export Proto_alpha.Environment.Raw_hashes.
Module Raw_hashes_check : Raw_hashes_signature := Raw_hashes.
Module Type Compare_signature.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S.
Record signature {t : Set} : Set := {
t := t;
[x = y] iff [compare x y = 0]
[x <> y] iff [compare x y <> 0]
[x < y] iff [compare x y < 0]
[x <= y] iff [compare x y <= 0]
[x >= y] iff [compare x y >= 0]
[x > y] iff [compare x y > 0]
[compare] an alias for the functor parameter's [compare] function
[equal x y] iff [compare x y = 0]
[max x y] is [x] if [x >= y] otherwise it is [y]
[min x y] is [x] if [x <= y] otherwise it is [y]
min : t → t → t;
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Parameter Make :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := P.(COMPARABLE.t)).
Parameter Char : S (t := ascii).
Parameter Bool : S (t := bool).
Module Int.
Definition t : Set := int.
Parameter op_eq : int → int → bool.
Parameter op_ltgt : int → int → bool.
Parameter op_lt : int → int → bool.
Parameter op_gt : int → int → bool.
Parameter op_lteq : int → int → bool.
Parameter op_gteq : int → int → bool.
Parameter compare : int → int → int.
Parameter max : int → int → int.
Parameter min : int → int → int.
Parameter equal : int → int → bool.
End Int.
Parameter Int32 : S (t := int32).
Parameter Uint32 : S (t := int32).
Parameter Int64 : S (t := int64).
Parameter Uint64 : S (t := int64).
Parameter String : S (t := string).
Parameter Bytes : S (t := bytes).
Parameter Z : S (t := Z.t).
Parameter List :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := list P.(COMPARABLE.t)).
Parameter Option :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := option P.(COMPARABLE.t)).
Parameter Result :
∀ {Ok_t Error_t : Set},
∀ (Ok : COMPARABLE (t := Ok_t)),
∀ (Error : COMPARABLE (t := Error_t)),
S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).
Module List_length_with.
Parameter op_eq : ∀ {a : Set}, list a → int → bool.
Parameter op_ltgt : ∀ {a : Set}, list a → int → bool.
Parameter op_lt : ∀ {a : Set}, list a → int → bool.
Parameter op_lteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gt : ∀ {a : Set}, list a → int → bool.
Parameter compare : ∀ {a : Set}, list a → int → int.
Parameter equal : ∀ {a : Set}, list a → int → bool.
End List_length_with.
Module List_lengths.
Parameter op_eq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_ltgt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gt : ∀ {a b : Set}, list a → list b → bool.
Parameter compare : ∀ {a b : Set}, list a → list b → int.
Parameter equal : ∀ {a b : Set}, list a → list b → bool.
End List_lengths.
Parameter or_else : int → (unit → int) → int.
End Compare_signature.
Require Export Proto_alpha.Environment.Compare.
Module Compare_check : Compare_signature := Compare.
Module Type Time_signature.
Parameter t : Set.
Parameter Included_S : Compare.S (t := t).
Definition op_eq : t → t → bool := Included_S.(Compare.S.op_eq).
Definition op_ltgt : t → t → bool := Included_S.(Compare.S.op_ltgt).
Definition op_lt : t → t → bool := Included_S.(Compare.S.op_lt).
Definition op_lteq : t → t → bool := Included_S.(Compare.S.op_lteq).
Definition op_gteq : t → t → bool := Included_S.(Compare.S.op_gteq).
Definition op_gt : t → t → bool := Included_S.(Compare.S.op_gt).
Definition compare : t → t → int := Included_S.(Compare.S.compare).
Definition equal : t → t → bool := Included_S.(Compare.S.equal).
Definition max : t → t → t := Included_S.(Compare.S.max).
Definition min : t → t → t := Included_S.(Compare.S.min).
Parameter add : t → int64 → t.
Parameter diff_value : t → t → int64.
Parameter of_seconds : int64 → t.
Parameter to_seconds : t → int64.
Parameter of_notation : string → option t.
Parameter of_notation_exn : string → t.
Parameter to_notation : t → string.
Parameter encoding : Data_encoding.t t.
Parameter rfc_encoding : Data_encoding.t t.
Parameter pp_hum : Format.formatter → t → unit.
End Time_signature.
Require Export Proto_alpha.Environment.Time.
Module Time_check : Time_signature := Time.
Module Type TzEndian_signature.
Parameter get_int32 : bytes → int → int32.
Parameter get_int32_string : string → int → int32.
Parameter set_int32 : bytes → int → int32 → unit.
Parameter set_int8 : bytes → int → int → unit.
Parameter get_int8 : bytes → int → int.
Parameter get_int8_string : string → int → int.
Parameter set_int16 : bytes → int → int → unit.
Parameter get_int16 : bytes → int → int.
Parameter get_int16_string : string → int → int.
Parameter set_int64 : bytes → int → int64 → unit.
Parameter get_int64 : bytes → int → int64.
Parameter get_int64_string : string → int → int64.
Parameter get_uint8 : bytes → int → int.
Parameter get_uint8_string : string → int → int.
Parameter set_uint8 : bytes → int → int → unit.
Parameter get_uint16 : bytes → int → int.
Parameter get_uint16_string : string → int → int.
Parameter set_uint16 : bytes → int → int → unit.
End TzEndian_signature.
Require Export Proto_alpha.Environment.TzEndian.
Module TzEndian_check : TzEndian_signature := TzEndian.
Module Type Bits_signature.
Parameter numbits : int → int.
End Bits_signature.
Require Export Proto_alpha.Environment.Bits.
Module Bits_check : Bits_signature := Bits.
Module Type Equality_witness_signature.
Inductive eq : Set :=
| Refl : eq.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, unit → t a.
Parameter eq_value : ∀ {a b : Set}, t a → t b → option eq.
Parameter hash_value : ∀ {a : Set}, t a → int.
End Equality_witness_signature.
Require Export Proto_alpha.Environment.Equality_witness.
Module Equality_witness_check : Equality_witness_signature := Equality_witness.
Module Type FallbackArray_signature.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, int → a → t a.
Parameter of_list : ∀ {a b : Set}, b → (a → b) → list a → t b.
Parameter fallback : ∀ {a : Set}, t a → a.
Parameter length : ∀ {a : Set}, t a → int.
Parameter get : ∀ {a : Set}, t a → int → a.
Parameter set : ∀ {a : Set}, t a → int → a → unit.
Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter fold : ∀ {a b : Set}, (b → a → b) → t a → b → b.
Parameter fold_map : ∀ {a b c : Set},
(b → a → b × c) → t a → b → c → b × t c.
End FallbackArray_signature.
Require Export Proto_alpha.Environment.FallbackArray.
Module FallbackArray_check : FallbackArray_signature := FallbackArray.
Module Type Error_monad_signature.
Inductive error_category : Set :=
| Outdated : error_category
| Permanent : error_category
| Temporary : error_category
| Branch : error_category.
Definition _error := extensible_type.
Parameter error_encoding : Data_encoding.t _error.
Parameter pp : Format.formatter → _error → unit.
Parameter register_error_kind : ∀ {err : Set},
error_category → string → string → string →
option (Format.formatter → err → unit) → Data_encoding.t err →
(_error → option err) → (err → _error) → unit.
Parameter json_of_error : _error → Data_encoding.json.
Parameter error_of_json : Data_encoding.json → _error.
Module error_info.
Record record : Set := Build {
category : error_category;
id : string;
title : string;
description : string;
schema : Data_encoding.json_schema;
}.
Definition with_category category (r : record) :=
Build category r.(id) r.(title) r.(description) r.(schema).
Definition with_id id (r : record) :=
Build r.(category) id r.(title) r.(description) r.(schema).
Definition with_title title (r : record) :=
Build r.(category) r.(id) title r.(description) r.(schema).
Definition with_description description (r : record) :=
Build r.(category) r.(id) r.(title) description r.(schema).
Definition with_schema schema (r : record) :=
Build r.(category) r.(id) r.(title) r.(description) schema.
End error_info.
Definition error_info := error_info.record.
Parameter pp_info : Format.formatter → error_info → unit.
Parameter get_registered_errors : unit → list error_info.
Parameter trace : ∀ (err : Set), Set.
Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).
Parameter make_trace_encoding : ∀ {_error : Set},
Data_encoding.t _error → Data_encoding.t (trace _error).
Parameter trace_encoding : Data_encoding.t (trace _error).
Parameter pp_trace : Format.formatter → trace _error → unit.
Parameter result_encoding : ∀ {a : Set},
Data_encoding.t a → Data_encoding.t (tzresult a).
Parameter ok : ∀ {a trace : Set}, a → Pervasives.result a trace.
Parameter _return : ∀ {a trace : Set}, a → Pervasives.result a trace.
Parameter return_unit : ∀ {trace : Set}, Pervasives.result unit trace.
Parameter return_none : ∀ {a trace : Set},
Pervasives.result (option a) trace.
Parameter return_some : ∀ {a trace : Set},
a → Pervasives.result (option a) trace.
Parameter return_nil : ∀ {a trace : Set},
Pervasives.result (list a) trace.
Parameter return_true : ∀ {trace : Set}, Pervasives.result bool trace.
Parameter return_false : ∀ {trace : Set}, Pervasives.result bool trace.
Parameter error_value : ∀ {a err : Set},
err → Pervasives.result a (trace err).
Parameter trace_of_error : ∀ {err : Set}, err → trace err.
Parameter fail : ∀ {a err : Set}, err → Pervasives.result a (trace err).
Parameter op_gtgteq : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_gtpipeeq : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_gtgtquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipequestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter op_gtgteqquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipeeqquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter op_gtgtquestioneq : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipequestioneq : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter record_trace : ∀ {a err : Set},
err → Pervasives.result a (trace err) → Pervasives.result a (trace err).
Parameter trace_value : ∀ {b err : Set},
err → Pervasives.result b (trace err) → Pervasives.result b (trace err).
Parameter record_trace_eval : ∀ {a err : Set},
(unit → err) → Pervasives.result a (trace err) →
Pervasives.result a (trace err).
Parameter trace_eval : ∀ {b err : Set},
(unit → err) → Pervasives.result b (trace err) →
Pervasives.result b (trace err).
Parameter error_unless : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter error_when : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter fail_unless : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter fail_when : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter unless : ∀ {trace : Set},
bool → (unit → Pervasives.result unit trace) →
Pervasives.result unit trace.
Parameter when_ : ∀ {trace : Set},
bool → (unit → Pervasives.result unit trace) →
Pervasives.result unit trace.
Parameter dont_wait : ∀ {trace : Set},
(extensible_type → unit) → (trace → unit) →
(unit → Pervasives.result unit trace) → unit.
Parameter catch : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter catch_f : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) →
(extensible_type → _error) → tzresult a.
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter join_e : ∀ {err : Set},
list (Pervasives.result unit (trace err)) →
Pervasives.result unit (trace err).
Parameter all_e : ∀ {a err : Set},
list (Pervasives.result a (trace err)) →
Pervasives.result (list a) (trace err).
Parameter both_e : ∀ {a b err : Set},
Pervasives.result a (trace err) → Pervasives.result b (trace err) →
Pervasives.result (a × b) (trace err).
Parameter shell_tztrace : Set.
Definition shell_tzresult (a : Set) : Set :=
Pervasives.result a shell_tztrace.
Module Lwt_syntax.
Parameter _return : ∀ {a : Set}, a → a.
Parameter return_none : ∀ {A : Set}, option A.
Parameter return_nil : ∀ {A : Set}, list A.
Parameter return_true : bool.
Parameter return_false : bool.
Parameter return_some : ∀ {a : Set}, a → option a.
Parameter return_ok : ∀ {B a : Set}, a → Pervasives.result a B.
Parameter return_error : ∀ {B e : Set}, e → Pervasives.result B e.
Parameter return_ok_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_ok_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_none : ∀ {a e : Set},
Pervasives.result (option a) e.
Parameter return_ok_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter op_letstar : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andstar : ∀ {a b : Set}, a → b → a × b.
Parameter op_letplus : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andplus : ∀ {a b : Set}, a → b → a × b.
Parameter join : list unit → unit.
Parameter all : ∀ {a : Set}, list a → list a.
Parameter both : ∀ {a b : Set}, a → b → a × b.
End Lwt_syntax.
Module Result_syntax.
Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.
Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.
Parameter return_some : ∀ {a e : Set},
a → Pervasives.result (option a) e.
Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Parameter both : ∀ {a b e : Set},
Pervasives.result a e → Pervasives.result b e →
Pervasives.result (a × b) (list e).
End Result_syntax.
Module Lwt_result_syntax.
Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.
Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.
Parameter return_some : ∀ {a e : Set},
a → Pervasives.result (option a) e.
Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter lwt_map_error : ∀ {a e f : Set},
(e → f) → Pervasives.result a e → Pervasives.result a f.
Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_letstarquestion : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Parameter both : ∀ {a b e : Set},
Pervasives.result a e → Pervasives.result b e →
Pervasives.result (a × b) (list e).
End Lwt_result_syntax.
Module Tzresult_syntax.
Parameter _return : ∀ {_error a : Set},
a → Pervasives.result a _error.
Parameter return_unit : ∀ {_error : Set},
Pervasives.result unit _error.
Parameter return_none : ∀ {_error a : Set},
Pervasives.result (option a) _error.
Parameter return_some : ∀ {_error a : Set},
a → Pervasives.result (option a) _error.
Parameter return_nil : ∀ {_error a : Set},
Pervasives.result (list a) _error.
Parameter return_true : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter return_false : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter fail : ∀ {_error a : Set},
_error → Pervasives.result a (trace _error).
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Tzresult_syntax.
Module Lwt_tzresult_syntax.
Parameter _return : ∀ {_error a : Set},
a → Pervasives.result a _error.
Parameter return_unit : ∀ {_error : Set},
Pervasives.result unit _error.
Parameter return_none : ∀ {_error a : Set},
Pervasives.result (option a) _error.
Parameter return_some : ∀ {_error a : Set},
a → Pervasives.result (option a) _error.
Parameter return_nil : ∀ {_error a : Set},
Pervasives.result (list a) _error.
Parameter return_true : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter return_false : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter fail : ∀ {_error a : Set},
_error → Pervasives.result a (trace _error).
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_letstarquestion : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Lwt_tzresult_syntax.
End Error_monad_signature.
Require Export Proto_alpha.Environment.Error_monad.
Module Error_monad_check : Error_monad_signature := Error_monad.
Export Error_monad.Notations.
Module Type Seq_signature.
Reserved Notation "'t".
Inductive node (a : Set) : Set :=
| Nil : node a
| Cons : a → 't a → node a
where "'t" := (fun (t_a : Set) ⇒ unit → node t_a).
Definition t := 't.
Arguments Nil {_}.
Arguments Cons {_}.
Parameter empty : ∀ {a : Set}, t a.
Parameter _return : ∀ {a : Set}, a → t a.
Parameter cons_value : ∀ {a : Set}, a → t a → t a.
Parameter append : ∀ {a : Set}, t a → t a → t a.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter filter : ∀ {a : Set}, (a → bool) → t a → t a.
Parameter filter_map : ∀ {a b : Set}, (a → option b) → t a → t b.
Parameter flat_map : ∀ {a b : Set}, (a → t b) → t a → t b.
Parameter fold_left : ∀ {a b : Set}, (a → b → a) → a → t b → a.
Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter unfold : ∀ {a b : Set}, (b → option (a × b)) → b → t a.
Parameter first : ∀ {a : Set}, t a → option a.
Parameter fold_left_e : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → t b →
Pervasives.result a trace.
Parameter fold_left_s : ∀ {a b : Set}, (a → b → a) → a → t b → a.
Parameter fold_left_es : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → t b →
Pervasives.result a trace.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.
Parameter iter_s : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.
Parameter iter_ep : ∀ {a : Set}, (a → M? unit) → t a → M? unit.
Parameter iter_p : ∀ {a : Set}, (a → unit) → t a → unit.
End Seq_signature.
Require Export Proto_alpha.Environment.Seq.
Module Seq_check : Seq_signature := Seq.
Module Type List_signature.
Definition t (a : Set) : Set := list a.
Parameter nil : ∀ {a : Set}, list a.
Parameter nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace.
Parameter nil_s : ∀ {a : Set}, list a.
Parameter nil_es : ∀ {a trace : Set}, Pervasives.result (list a) trace.
Parameter cons_value : ∀ {a : Set}, a → list a → list a.
Parameter hd : ∀ {a : Set}, list a → option a.
Parameter tl : ∀ {a : Set}, list a → option (list a).
Parameter nth : ∀ {a : Set}, list a → int → option a.
Parameter nth_opt : ∀ {a : Set}, list a → int → option a.
Parameter last : ∀ {a : Set}, a → list a → a.
Parameter last_opt : ∀ {a : Set}, list a → option a.
Parameter find : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_opt : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_map : ∀ {a b : Set},
(a → option b) → list a → option b.
Parameter mem : ∀ {a : Set}, (a → a → bool) → a → list a → bool.
Parameter assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b.
Parameter assoc_opt : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b.
Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.
Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.
Parameter mem_assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → bool.
Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.
Parameter remove_assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → list (a × b).
Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).
Parameter init_value : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter length : ∀ {a : Set}, list a → int.
Parameter rev : ∀ {a : Set}, list a → list a.
Parameter concat : ∀ {a : Set}, list (list a) → list a.
Parameter append : ∀ {a : Set}, list a → list a → list a.
Parameter rev_append : ∀ {a : Set}, list a → list a → list a.
Parameter flatten : ∀ {a : Set}, list (list a) → list a.
Parameter combine : ∀ {a b trace : Set},
trace → list a → list b → Pervasives.result (list (a × b)) trace.
Parameter rev_combine : ∀ {a b trace : Set},
trace → list a → list b → Pervasives.result (list (a × b)) trace.
Parameter split : ∀ {a b : Set}, list (a × b) → list a × list b.
Parameter iter2 : ∀ {a b trace : Set},
trace → (a → b → unit) → list a → list b →
Pervasives.result unit trace.
Parameter map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace.
Parameter rev_map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace.
Parameter fold_left2 : ∀ {a b c trace : Set},
trace → (a → b → c → a) → a → list b → list c →
Pervasives.result a trace.
Parameter fold_right2 : ∀ {a b c trace : Set},
trace → (a → b → c → c) → list a → list b → c →
Pervasives.result c trace.
Parameter for_all2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace.
Parameter _exists2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace.
Parameter init_e : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace.
Parameter init_s : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter init_es : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace.
Parameter init_p : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter find_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace.
Parameter find_s : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace.
Parameter find_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace.
Parameter find_map_s : ∀ {a b : Set},
(a → option b) → list a → option b.
Parameter find_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace.
Parameter filter : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter filteri : ∀ {a : Set}, (int → a → bool) → list a → list a.
Parameter find_all : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filter : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filteri : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter rev_filter_some : ∀ {a : Set}, list (option a) → list a.
Parameter filter_some : ∀ {a : Set}, list (option a) → list a.
Parameter rev_filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a.
Parameter filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a.
Parameter rev_filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b.
Parameter filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b.
Parameter rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.
Parameter filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.
Parameter rev_filter_right : ∀ {a b : Set},
list (Either.t a b) → list b.
Parameter filter_right : ∀ {a b : Set}, list (Either.t a b) → list b.
Parameter rev_filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filter_s : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter filter_s : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter rev_filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_partition : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter partition : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter rev_partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b.
Parameter partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b.
Parameter rev_partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b.
Parameter partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b.
Parameter rev_partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter rev_partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_p : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter rev_partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter rev_partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter iter : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iter_s : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iter_p : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iteri : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter iteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iteri_s : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter iteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iteri_p : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter map : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter map_s : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter map_p : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter mapi : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter mapi_s : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter mapi_p : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter rev_map : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_mapi : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter rev_map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_map_s : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_map_p : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b.
Parameter rev_mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b.
Parameter rev_filter_map : ∀ {a b : Set},
(a → option b) → list a → list b.
Parameter rev_filter_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace.
Parameter filter_map_e : ∀ {a b trace : Set},
(
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Parameter Make :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := P.(COMPARABLE.t)).
Parameter Char : S (t := ascii).
Parameter Bool : S (t := bool).
Module Int.
Definition t : Set := int.
Parameter op_eq : int → int → bool.
Parameter op_ltgt : int → int → bool.
Parameter op_lt : int → int → bool.
Parameter op_gt : int → int → bool.
Parameter op_lteq : int → int → bool.
Parameter op_gteq : int → int → bool.
Parameter compare : int → int → int.
Parameter max : int → int → int.
Parameter min : int → int → int.
Parameter equal : int → int → bool.
End Int.
Parameter Int32 : S (t := int32).
Parameter Uint32 : S (t := int32).
Parameter Int64 : S (t := int64).
Parameter Uint64 : S (t := int64).
Parameter String : S (t := string).
Parameter Bytes : S (t := bytes).
Parameter Z : S (t := Z.t).
Parameter List :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := list P.(COMPARABLE.t)).
Parameter Option :
∀ {P_t : Set},
∀ (P : COMPARABLE (t := P_t)), S (t := option P.(COMPARABLE.t)).
Parameter Result :
∀ {Ok_t Error_t : Set},
∀ (Ok : COMPARABLE (t := Ok_t)),
∀ (Error : COMPARABLE (t := Error_t)),
S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).
Module List_length_with.
Parameter op_eq : ∀ {a : Set}, list a → int → bool.
Parameter op_ltgt : ∀ {a : Set}, list a → int → bool.
Parameter op_lt : ∀ {a : Set}, list a → int → bool.
Parameter op_lteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gt : ∀ {a : Set}, list a → int → bool.
Parameter compare : ∀ {a : Set}, list a → int → int.
Parameter equal : ∀ {a : Set}, list a → int → bool.
End List_length_with.
Module List_lengths.
Parameter op_eq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_ltgt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gt : ∀ {a b : Set}, list a → list b → bool.
Parameter compare : ∀ {a b : Set}, list a → list b → int.
Parameter equal : ∀ {a b : Set}, list a → list b → bool.
End List_lengths.
Parameter or_else : int → (unit → int) → int.
End Compare_signature.
Require Export Proto_alpha.Environment.Compare.
Module Compare_check : Compare_signature := Compare.
Module Type Time_signature.
Parameter t : Set.
Parameter Included_S : Compare.S (t := t).
Definition op_eq : t → t → bool := Included_S.(Compare.S.op_eq).
Definition op_ltgt : t → t → bool := Included_S.(Compare.S.op_ltgt).
Definition op_lt : t → t → bool := Included_S.(Compare.S.op_lt).
Definition op_lteq : t → t → bool := Included_S.(Compare.S.op_lteq).
Definition op_gteq : t → t → bool := Included_S.(Compare.S.op_gteq).
Definition op_gt : t → t → bool := Included_S.(Compare.S.op_gt).
Definition compare : t → t → int := Included_S.(Compare.S.compare).
Definition equal : t → t → bool := Included_S.(Compare.S.equal).
Definition max : t → t → t := Included_S.(Compare.S.max).
Definition min : t → t → t := Included_S.(Compare.S.min).
Parameter add : t → int64 → t.
Parameter diff_value : t → t → int64.
Parameter of_seconds : int64 → t.
Parameter to_seconds : t → int64.
Parameter of_notation : string → option t.
Parameter of_notation_exn : string → t.
Parameter to_notation : t → string.
Parameter encoding : Data_encoding.t t.
Parameter rfc_encoding : Data_encoding.t t.
Parameter pp_hum : Format.formatter → t → unit.
End Time_signature.
Require Export Proto_alpha.Environment.Time.
Module Time_check : Time_signature := Time.
Module Type TzEndian_signature.
Parameter get_int32 : bytes → int → int32.
Parameter get_int32_string : string → int → int32.
Parameter set_int32 : bytes → int → int32 → unit.
Parameter set_int8 : bytes → int → int → unit.
Parameter get_int8 : bytes → int → int.
Parameter get_int8_string : string → int → int.
Parameter set_int16 : bytes → int → int → unit.
Parameter get_int16 : bytes → int → int.
Parameter get_int16_string : string → int → int.
Parameter set_int64 : bytes → int → int64 → unit.
Parameter get_int64 : bytes → int → int64.
Parameter get_int64_string : string → int → int64.
Parameter get_uint8 : bytes → int → int.
Parameter get_uint8_string : string → int → int.
Parameter set_uint8 : bytes → int → int → unit.
Parameter get_uint16 : bytes → int → int.
Parameter get_uint16_string : string → int → int.
Parameter set_uint16 : bytes → int → int → unit.
End TzEndian_signature.
Require Export Proto_alpha.Environment.TzEndian.
Module TzEndian_check : TzEndian_signature := TzEndian.
Module Type Bits_signature.
Parameter numbits : int → int.
End Bits_signature.
Require Export Proto_alpha.Environment.Bits.
Module Bits_check : Bits_signature := Bits.
Module Type Equality_witness_signature.
Inductive eq : Set :=
| Refl : eq.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, unit → t a.
Parameter eq_value : ∀ {a b : Set}, t a → t b → option eq.
Parameter hash_value : ∀ {a : Set}, t a → int.
End Equality_witness_signature.
Require Export Proto_alpha.Environment.Equality_witness.
Module Equality_witness_check : Equality_witness_signature := Equality_witness.
Module Type FallbackArray_signature.
Parameter t : ∀ (a : Set), Set.
Parameter make : ∀ {a : Set}, int → a → t a.
Parameter of_list : ∀ {a b : Set}, b → (a → b) → list a → t b.
Parameter fallback : ∀ {a : Set}, t a → a.
Parameter length : ∀ {a : Set}, t a → int.
Parameter get : ∀ {a : Set}, t a → int → a.
Parameter set : ∀ {a : Set}, t a → int → a → unit.
Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter fold : ∀ {a b : Set}, (b → a → b) → t a → b → b.
Parameter fold_map : ∀ {a b c : Set},
(b → a → b × c) → t a → b → c → b × t c.
End FallbackArray_signature.
Require Export Proto_alpha.Environment.FallbackArray.
Module FallbackArray_check : FallbackArray_signature := FallbackArray.
Module Type Error_monad_signature.
Inductive error_category : Set :=
| Outdated : error_category
| Permanent : error_category
| Temporary : error_category
| Branch : error_category.
Definition _error := extensible_type.
Parameter error_encoding : Data_encoding.t _error.
Parameter pp : Format.formatter → _error → unit.
Parameter register_error_kind : ∀ {err : Set},
error_category → string → string → string →
option (Format.formatter → err → unit) → Data_encoding.t err →
(_error → option err) → (err → _error) → unit.
Parameter json_of_error : _error → Data_encoding.json.
Parameter error_of_json : Data_encoding.json → _error.
Module error_info.
Record record : Set := Build {
category : error_category;
id : string;
title : string;
description : string;
schema : Data_encoding.json_schema;
}.
Definition with_category category (r : record) :=
Build category r.(id) r.(title) r.(description) r.(schema).
Definition with_id id (r : record) :=
Build r.(category) id r.(title) r.(description) r.(schema).
Definition with_title title (r : record) :=
Build r.(category) r.(id) title r.(description) r.(schema).
Definition with_description description (r : record) :=
Build r.(category) r.(id) r.(title) description r.(schema).
Definition with_schema schema (r : record) :=
Build r.(category) r.(id) r.(title) r.(description) schema.
End error_info.
Definition error_info := error_info.record.
Parameter pp_info : Format.formatter → error_info → unit.
Parameter get_registered_errors : unit → list error_info.
Parameter trace : ∀ (err : Set), Set.
Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).
Parameter make_trace_encoding : ∀ {_error : Set},
Data_encoding.t _error → Data_encoding.t (trace _error).
Parameter trace_encoding : Data_encoding.t (trace _error).
Parameter pp_trace : Format.formatter → trace _error → unit.
Parameter result_encoding : ∀ {a : Set},
Data_encoding.t a → Data_encoding.t (tzresult a).
Parameter ok : ∀ {a trace : Set}, a → Pervasives.result a trace.
Parameter _return : ∀ {a trace : Set}, a → Pervasives.result a trace.
Parameter return_unit : ∀ {trace : Set}, Pervasives.result unit trace.
Parameter return_none : ∀ {a trace : Set},
Pervasives.result (option a) trace.
Parameter return_some : ∀ {a trace : Set},
a → Pervasives.result (option a) trace.
Parameter return_nil : ∀ {a trace : Set},
Pervasives.result (list a) trace.
Parameter return_true : ∀ {trace : Set}, Pervasives.result bool trace.
Parameter return_false : ∀ {trace : Set}, Pervasives.result bool trace.
Parameter error_value : ∀ {a err : Set},
err → Pervasives.result a (trace err).
Parameter trace_of_error : ∀ {err : Set}, err → trace err.
Parameter fail : ∀ {a err : Set}, err → Pervasives.result a (trace err).
Parameter op_gtgteq : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_gtpipeeq : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_gtgtquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipequestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter op_gtgteqquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipeeqquestion : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter op_gtgtquestioneq : ∀ {a b trace : Set},
Pervasives.result a trace → (a → Pervasives.result b trace) →
Pervasives.result b trace.
Parameter op_gtpipequestioneq : ∀ {a b trace : Set},
Pervasives.result a trace → (a → b) → Pervasives.result b trace.
Parameter record_trace : ∀ {a err : Set},
err → Pervasives.result a (trace err) → Pervasives.result a (trace err).
Parameter trace_value : ∀ {b err : Set},
err → Pervasives.result b (trace err) → Pervasives.result b (trace err).
Parameter record_trace_eval : ∀ {a err : Set},
(unit → err) → Pervasives.result a (trace err) →
Pervasives.result a (trace err).
Parameter trace_eval : ∀ {b err : Set},
(unit → err) → Pervasives.result b (trace err) →
Pervasives.result b (trace err).
Parameter error_unless : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter error_when : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter fail_unless : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter fail_when : ∀ {err : Set},
bool → err → Pervasives.result unit (trace err).
Parameter unless : ∀ {trace : Set},
bool → (unit → Pervasives.result unit trace) →
Pervasives.result unit trace.
Parameter when_ : ∀ {trace : Set},
bool → (unit → Pervasives.result unit trace) →
Pervasives.result unit trace.
Parameter dont_wait : ∀ {trace : Set},
(extensible_type → unit) → (trace → unit) →
(unit → Pervasives.result unit trace) → unit.
Parameter catch : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter catch_f : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) →
(extensible_type → _error) → tzresult a.
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter join_e : ∀ {err : Set},
list (Pervasives.result unit (trace err)) →
Pervasives.result unit (trace err).
Parameter all_e : ∀ {a err : Set},
list (Pervasives.result a (trace err)) →
Pervasives.result (list a) (trace err).
Parameter both_e : ∀ {a b err : Set},
Pervasives.result a (trace err) → Pervasives.result b (trace err) →
Pervasives.result (a × b) (trace err).
Parameter shell_tztrace : Set.
Definition shell_tzresult (a : Set) : Set :=
Pervasives.result a shell_tztrace.
Module Lwt_syntax.
Parameter _return : ∀ {a : Set}, a → a.
Parameter return_none : ∀ {A : Set}, option A.
Parameter return_nil : ∀ {A : Set}, list A.
Parameter return_true : bool.
Parameter return_false : bool.
Parameter return_some : ∀ {a : Set}, a → option a.
Parameter return_ok : ∀ {B a : Set}, a → Pervasives.result a B.
Parameter return_error : ∀ {B e : Set}, e → Pervasives.result B e.
Parameter return_ok_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_ok_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_none : ∀ {a e : Set},
Pervasives.result (option a) e.
Parameter return_ok_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter op_letstar : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andstar : ∀ {a b : Set}, a → b → a × b.
Parameter op_letplus : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andplus : ∀ {a b : Set}, a → b → a × b.
Parameter join : list unit → unit.
Parameter all : ∀ {a : Set}, list a → list a.
Parameter both : ∀ {a b : Set}, a → b → a × b.
End Lwt_syntax.
Module Result_syntax.
Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.
Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.
Parameter return_some : ∀ {a e : Set},
a → Pervasives.result (option a) e.
Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Parameter both : ∀ {a b e : Set},
Pervasives.result a e → Pervasives.result b e →
Pervasives.result (a × b) (list e).
End Result_syntax.
Module Lwt_result_syntax.
Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.
Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.
Parameter return_some : ∀ {a e : Set},
a → Pervasives.result (option a) e.
Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter lwt_map_error : ∀ {a e f : Set},
(e → f) → Pervasives.result a e → Pervasives.result a f.
Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_letstarquestion : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Parameter both : ∀ {a b e : Set},
Pervasives.result a e → Pervasives.result b e →
Pervasives.result (a × b) (list e).
End Lwt_result_syntax.
Module Tzresult_syntax.
Parameter _return : ∀ {_error a : Set},
a → Pervasives.result a _error.
Parameter return_unit : ∀ {_error : Set},
Pervasives.result unit _error.
Parameter return_none : ∀ {_error a : Set},
Pervasives.result (option a) _error.
Parameter return_some : ∀ {_error a : Set},
a → Pervasives.result (option a) _error.
Parameter return_nil : ∀ {_error a : Set},
Pervasives.result (list a) _error.
Parameter return_true : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter return_false : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter fail : ∀ {_error a : Set},
_error → Pervasives.result a (trace _error).
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Tzresult_syntax.
Module Lwt_tzresult_syntax.
Parameter _return : ∀ {_error a : Set},
a → Pervasives.result a _error.
Parameter return_unit : ∀ {_error : Set},
Pervasives.result unit _error.
Parameter return_none : ∀ {_error a : Set},
Pervasives.result (option a) _error.
Parameter return_some : ∀ {_error a : Set},
a → Pervasives.result (option a) _error.
Parameter return_nil : ∀ {_error a : Set},
Pervasives.result (list a) _error.
Parameter return_true : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter return_false : ∀ {_error : Set},
Pervasives.result bool _error.
Parameter fail : ∀ {_error a : Set},
_error → Pervasives.result a (trace _error).
Parameter op_letstar : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letplus : ∀ {a b e : Set},
Pervasives.result a e → (a → b) → Pervasives.result b e.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_letstarquestion : ∀ {a b e : Set},
Pervasives.result a e → (a → Pervasives.result b e) →
Pervasives.result b e.
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Lwt_tzresult_syntax.
End Error_monad_signature.
Require Export Proto_alpha.Environment.Error_monad.
Module Error_monad_check : Error_monad_signature := Error_monad.
Export Error_monad.Notations.
Module Type Seq_signature.
Reserved Notation "'t".
Inductive node (a : Set) : Set :=
| Nil : node a
| Cons : a → 't a → node a
where "'t" := (fun (t_a : Set) ⇒ unit → node t_a).
Definition t := 't.
Arguments Nil {_}.
Arguments Cons {_}.
Parameter empty : ∀ {a : Set}, t a.
Parameter _return : ∀ {a : Set}, a → t a.
Parameter cons_value : ∀ {a : Set}, a → t a → t a.
Parameter append : ∀ {a : Set}, t a → t a → t a.
Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.
Parameter filter : ∀ {a : Set}, (a → bool) → t a → t a.
Parameter filter_map : ∀ {a b : Set}, (a → option b) → t a → t b.
Parameter flat_map : ∀ {a b : Set}, (a → t b) → t a → t b.
Parameter fold_left : ∀ {a b : Set}, (a → b → a) → a → t b → a.
Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter unfold : ∀ {a b : Set}, (b → option (a × b)) → b → t a.
Parameter first : ∀ {a : Set}, t a → option a.
Parameter fold_left_e : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → t b →
Pervasives.result a trace.
Parameter fold_left_s : ∀ {a b : Set}, (a → b → a) → a → t b → a.
Parameter fold_left_es : ∀ {a b trace : Set},
(a → b → Pervasives.result a trace) → a → t b →
Pervasives.result a trace.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.
Parameter iter_s : ∀ {a : Set}, (a → unit) → t a → unit.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.
Parameter iter_ep : ∀ {a : Set}, (a → M? unit) → t a → M? unit.
Parameter iter_p : ∀ {a : Set}, (a → unit) → t a → unit.
End Seq_signature.
Require Export Proto_alpha.Environment.Seq.
Module Seq_check : Seq_signature := Seq.
Module Type List_signature.
Definition t (a : Set) : Set := list a.
Parameter nil : ∀ {a : Set}, list a.
Parameter nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace.
Parameter nil_s : ∀ {a : Set}, list a.
Parameter nil_es : ∀ {a trace : Set}, Pervasives.result (list a) trace.
Parameter cons_value : ∀ {a : Set}, a → list a → list a.
Parameter hd : ∀ {a : Set}, list a → option a.
Parameter tl : ∀ {a : Set}, list a → option (list a).
Parameter nth : ∀ {a : Set}, list a → int → option a.
Parameter nth_opt : ∀ {a : Set}, list a → int → option a.
Parameter last : ∀ {a : Set}, a → list a → a.
Parameter last_opt : ∀ {a : Set}, list a → option a.
Parameter find : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_opt : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_map : ∀ {a b : Set},
(a → option b) → list a → option b.
Parameter mem : ∀ {a : Set}, (a → a → bool) → a → list a → bool.
Parameter assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b.
Parameter assoc_opt : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → option b.
Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.
Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.
Parameter mem_assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → bool.
Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.
Parameter remove_assoc : ∀ {a b : Set},
(a → a → bool) → a → list (a × b) → list (a × b).
Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).
Parameter init_value : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter length : ∀ {a : Set}, list a → int.
Parameter rev : ∀ {a : Set}, list a → list a.
Parameter concat : ∀ {a : Set}, list (list a) → list a.
Parameter append : ∀ {a : Set}, list a → list a → list a.
Parameter rev_append : ∀ {a : Set}, list a → list a → list a.
Parameter flatten : ∀ {a : Set}, list (list a) → list a.
Parameter combine : ∀ {a b trace : Set},
trace → list a → list b → Pervasives.result (list (a × b)) trace.
Parameter rev_combine : ∀ {a b trace : Set},
trace → list a → list b → Pervasives.result (list (a × b)) trace.
Parameter split : ∀ {a b : Set}, list (a × b) → list a × list b.
Parameter iter2 : ∀ {a b trace : Set},
trace → (a → b → unit) → list a → list b →
Pervasives.result unit trace.
Parameter map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace.
Parameter rev_map2 : ∀ {a b c trace : Set},
trace → (a → b → c) → list a → list b →
Pervasives.result (list c) trace.
Parameter fold_left2 : ∀ {a b c trace : Set},
trace → (a → b → c → a) → a → list b → list c →
Pervasives.result a trace.
Parameter fold_right2 : ∀ {a b c trace : Set},
trace → (a → b → c → c) → list a → list b → c →
Pervasives.result c trace.
Parameter for_all2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace.
Parameter _exists2 : ∀ {a b trace : Set},
trace → (a → b → bool) → list a → list b →
Pervasives.result bool trace.
Parameter init_e : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace.
Parameter init_s : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter init_es : ∀ {a trace : Set},
trace → int → (int → Pervasives.result a trace) →
Pervasives.result (list a) trace.
Parameter init_p : ∀ {a trace : Set},
trace → int → (int → a) → Pervasives.result (list a) trace.
Parameter find_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace.
Parameter find_s : ∀ {a : Set}, (a → bool) → list a → option a.
Parameter find_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (option a) trace.
Parameter find_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace.
Parameter find_map_s : ∀ {a b : Set},
(a → option b) → list a → option b.
Parameter find_map_es : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (option b) trace.
Parameter filter : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter filteri : ∀ {a : Set}, (int → a → bool) → list a → list a.
Parameter find_all : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filter : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filteri : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter rev_filter_some : ∀ {a : Set}, list (option a) → list a.
Parameter filter_some : ∀ {a : Set}, list (option a) → list a.
Parameter rev_filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a.
Parameter filter_ok : ∀ {a b : Set},
list (Pervasives.result a b) → list a.
Parameter rev_filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b.
Parameter filter_error : ∀ {a b : Set},
list (Pervasives.result a b) → list b.
Parameter rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.
Parameter filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.
Parameter rev_filter_right : ∀ {a b : Set},
list (Either.t a b) → list b.
Parameter filter_right : ∀ {a b : Set}, list (Either.t a b) → list b.
Parameter rev_filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filter_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filter_s : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter filter_s : ∀ {a : Set}, (a → bool) → list a → list a.
Parameter rev_filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filter_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter filteri_s : ∀ {a : Set},
(int → a → bool) → list a → list a.
Parameter rev_filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter filteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result bool trace) → list a →
Pervasives.result (list a) trace.
Parameter rev_partition : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter partition : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter partition_map : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter rev_partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b.
Parameter partition_result : ∀ {a b : Set},
list (Pervasives.result a b) → list a × list b.
Parameter rev_partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b.
Parameter partition_either : ∀ {a b : Set},
list (Either.t a b) → list a × list b.
Parameter rev_partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_e : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter rev_partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter partition_s : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_es : ∀ {a trace : Set},
(a → Pervasives.result bool trace) → list a →
Pervasives.result (list a × list a) trace.
Parameter partition_p : ∀ {a : Set},
(a → bool) → list a → list a × list a.
Parameter rev_partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter partition_map_e : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter rev_partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter partition_map_s : ∀ {a b c : Set},
(a → Either.t b c) → list a → list b × list c.
Parameter rev_partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter partition_map_es : ∀ {a b c trace : Set},
(a → Pervasives.result (Either.t b c) trace) → list a →
Pervasives.result (list b × list c) trace.
Parameter iter : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iter_s : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iter_p : ∀ {a : Set}, (a → unit) → list a → unit.
Parameter iteri : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter iteri_e : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iteri_s : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter iteri_es : ∀ {a trace : Set},
(int → a → Pervasives.result unit trace) → list a →
Pervasives.result unit trace.
Parameter iteri_p : ∀ {a : Set}, (int → a → unit) → list a → unit.
Parameter map : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter map_s : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter map_p : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter mapi : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter mapi_s : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter mapi_p : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter rev_map : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_mapi : ∀ {a b : Set}, (int → a → b) → list a → list b.
Parameter rev_map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_map_s : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_map_p : ∀ {a b : Set}, (a → b) → list a → list b.
Parameter rev_mapi_e : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_mapi_s : ∀ {a b : Set},
(int → a → b) → list a → list b.
Parameter rev_mapi_es : ∀ {a b trace : Set},
(int → a → Pervasives.result b trace) → list a →
Pervasives.result (list b) trace.
Parameter rev_mapi_p : ∀ {a b : Set},
(int → a → b) → list a → list b.
Parameter rev_filter_map : ∀ {a b : Set},
(a → option b) → list a → list b.
Parameter rev_filter_map_e : ∀ {a b trace : Set},
(a → Pervasives.result (option b) trace) → list a →
Pervasives.result (list b) trace.
Parameter filter_map_e : ∀ {a b trace : Set},
(