🍃 Blake2B.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Module Name.
Record signature : Set := {
name : string;
title : string;
size_value : option int;
}.
End Name.
Definition Name := @Name.signature.
Module PrefixedName.
Record signature : Set := {
name : string;
title : string;
size_value : option int;
b58check_prefix : string;
}.
End PrefixedName.
Definition PrefixedName := @PrefixedName.signature.
Parameter Make_minimal_t : ∀ (Name : Name), Set.
Parameter Make_minimal :
∀ (Name : Name), S.MINIMAL_HASH (t := Make_minimal_t Name).
Module Register.
Record signature : Set := {
register_encoding :
∀ {a : Set},
string → int → (a → string) → (string → option a) →
(a → Base58.data) → Base58.encoding a;
}.
End Register.
Definition Register := @Register.signature.
Parameter Make_t : ∀ (Register : Register) (Name : PrefixedName), Set.
Parameter Make_Set_t :
∀ (Register : Register) (Name : PrefixedName), Set.
Parameter Make_Map_t :
∀ (Register : Register) (Name : PrefixedName), Set → Set.
Parameter Make :
∀ (Register : Register),
∀ (Name : PrefixedName),
S.HASH (t := Make_t Register Name) (Set_t := Make_Set_t Register Name)
(Map_t := Make_Map_t Register Name).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Module Name.
Record signature : Set := {
name : string;
title : string;
size_value : option int;
}.
End Name.
Definition Name := @Name.signature.
Module PrefixedName.
Record signature : Set := {
name : string;
title : string;
size_value : option int;
b58check_prefix : string;
}.
End PrefixedName.
Definition PrefixedName := @PrefixedName.signature.
Parameter Make_minimal_t : ∀ (Name : Name), Set.
Parameter Make_minimal :
∀ (Name : Name), S.MINIMAL_HASH (t := Make_minimal_t Name).
Module Register.
Record signature : Set := {
register_encoding :
∀ {a : Set},
string → int → (a → string) → (string → option a) →
(a → Base58.data) → Base58.encoding a;
}.
End Register.
Definition Register := @Register.signature.
Parameter Make_t : ∀ (Register : Register) (Name : PrefixedName), Set.
Parameter Make_Set_t :
∀ (Register : Register) (Name : PrefixedName), Set.
Parameter Make_Map_t :
∀ (Register : Register) (Name : PrefixedName), Set → Set.
Parameter Make :
∀ (Register : Register),
∀ (Name : PrefixedName),
S.HASH (t := Make_t Register Name) (Set_t := Make_Set_t Register Name)
(Map_t := Make_Map_t Register Name).