🇿 Zk_rollup_scalar.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.

Definition t : Set := Bls.Primitive.Fr.(S.PRIME_FIELD.t).

Definition of_z (z_value : Z.t) : Bls.Primitive.Fr.(S.PRIME_FIELD.t) :=
  Bls.Primitive.Fr.(S.PRIME_FIELD.of_z) z_value.

Definition of_bits (bs : string) : Bls.Primitive.Fr.(S.PRIME_FIELD.t) :=
  let z_value := Z.of_bits bs in
  of_z z_value.