🍃 Bytes.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.Structs.V0.String.
Definition length : bytes → int := String.length.
Definition get : bytes → int → ascii := String.get.
Parameter set : bytes → int → ascii → unit.
Parameter make : int → ascii → bytes.
Parameter init_value : int → (int → ascii) → bytes.
Definition empty : bytes := "".
Definition copy : bytes → bytes := fun b ⇒ b.
Definition of_string : string → bytes := fun b ⇒ b.
Definition to_string : bytes → string := fun b ⇒ b.
Definition sub : bytes → int → int → bytes := String.sub.
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.
Definition cat : bytes → bytes → bytes :=
String.append.
Parameter iter : (ascii → unit) → bytes → unit.
Definition iteri : (int → ascii → unit) → bytes → unit := String.iteri.
Definition map : (ascii → ascii) → bytes → bytes := String.map.
Definition mapi : (int → ascii → ascii) → bytes → bytes := String.mapi.
Definition trim : bytes → bytes := String.trim.
Definition escaped : bytes → bytes := String.escaped.
Definition index_opt : bytes → ascii → option int := String.index_opt.
Definition rindex_opt : bytes → ascii → option int := String.rindex_opt.
Definition index_from_opt : bytes → int → ascii → option int := String.index_from_opt.
Definition rindex_from_opt : bytes → int → ascii → option int := String.rindex_from_opt.
Definition contains : bytes → ascii → bool := String.contains.
Definition contains_from : bytes → int → ascii → bool := String.contains_from.
Definition rcontains_from : bytes → int → ascii → bool := String.rcontains_from.
Definition uppercase_ascii : bytes → bytes := String.uppercase_ascii.
Definition lowercase_ascii : bytes → bytes := String.lowercase_ascii.
Definition capitalize_ascii : bytes → bytes := String.capitalize_ascii.
Definition uncapitalize_ascii : bytes → bytes := String.uncapitalize_ascii.
Definition t : Set := bytes.
Definition compare : t → t → int := String.compare.
Definition equal : t → t → bool := String.equal.
Parameter logand : bytes → bytes → bytes.
Parameter logor : bytes → bytes → bytes.
Parameter logxor : bytes → bytes → bytes.
Parameter lognot : bytes → bytes.
Parameter shift_left : bytes → int → bytes.
Parameter shift_right : bytes → int → bytes.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.Structs.V0.String.
Definition length : bytes → int := String.length.
Definition get : bytes → int → ascii := String.get.
Parameter set : bytes → int → ascii → unit.
Parameter make : int → ascii → bytes.
Parameter init_value : int → (int → ascii) → bytes.
Definition empty : bytes := "".
Definition copy : bytes → bytes := fun b ⇒ b.
Definition of_string : string → bytes := fun b ⇒ b.
Definition to_string : bytes → string := fun b ⇒ b.
Definition sub : bytes → int → int → bytes := String.sub.
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.
Definition cat : bytes → bytes → bytes :=
String.append.
Parameter iter : (ascii → unit) → bytes → unit.
Definition iteri : (int → ascii → unit) → bytes → unit := String.iteri.
Definition map : (ascii → ascii) → bytes → bytes := String.map.
Definition mapi : (int → ascii → ascii) → bytes → bytes := String.mapi.
Definition trim : bytes → bytes := String.trim.
Definition escaped : bytes → bytes := String.escaped.
Definition index_opt : bytes → ascii → option int := String.index_opt.
Definition rindex_opt : bytes → ascii → option int := String.rindex_opt.
Definition index_from_opt : bytes → int → ascii → option int := String.index_from_opt.
Definition rindex_from_opt : bytes → int → ascii → option int := String.rindex_from_opt.
Definition contains : bytes → ascii → bool := String.contains.
Definition contains_from : bytes → int → ascii → bool := String.contains_from.
Definition rcontains_from : bytes → int → ascii → bool := String.rcontains_from.
Definition uppercase_ascii : bytes → bytes := String.uppercase_ascii.
Definition lowercase_ascii : bytes → bytes := String.lowercase_ascii.
Definition capitalize_ascii : bytes → bytes := String.capitalize_ascii.
Definition uncapitalize_ascii : bytes → bytes := String.uncapitalize_ascii.
Definition t : Set := bytes.
Definition compare : t → t → int := String.compare.
Definition equal : t → t → bool := String.equal.
Parameter logand : bytes → bytes → bytes.
Parameter logor : bytes → bytes → bytes.
Parameter logxor : bytes → bytes → bytes.
Parameter lognot : bytes → bytes.
Parameter shift_left : bytes → int → bytes.
Parameter shift_right : bytes → int → bytes.