Skip to main content

🍃 Base58.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Parameter encoding : (a : Set), Set.

Parameter simple_decode : {a : Set}, encoding a string option a.

Parameter simple_encode : {a : Set}, encoding a a string.

Definition data : Set := extensible_type.

Parameter register_encoding : {a : Set},
  string int (a string) (string option a) (a data)
  encoding a.

Parameter check_encoded_prefix : {a : Set},
  encoding a string int unit.

Parameter decode : string option data.