val print_lbytes: display:bool -> len:size_nat -> lbytes len -> FStar.All.ML unit
let print_lbytes flag len b =
  if not flag then () else (
  let q = 32 in
  let n = len / q in
  let r = len % q in
  if n = 0 then (
    List.iter (fun a -> print_uint8_hex_pad a) (to_list b))
  else (
  repeat_range_all_ml 0 n (fun i _ ->
    let sb = sub #uint8 #len b (i * q) q in
    List.iter (fun a -> print_uint8_hex_pad a) (to_list sb);
    (if i < n - 1 then IO.print_string "\n" else ())) ();
  (if r <> 0 then IO.print_newline ());
  let sb = sub #uint8 #len b (n * q) r in
  List.iter (fun a -> print_uint8_hex_pad a) (to_list sb)))
val print_lbytes: display:bool -> len:size_nat -> lbytes len -> FStar.All.ML unit
let print_lbytes flag len b =
if not flag
then ()
else
  (let q = 32 in
    let n = len / q in
    let r = len % q in
    if n = 0
    then (List.iter (fun a -> print_uint8_hex_pad a) (to_list b))
    else
      (repeat_range_all_ml 0
          n
          (fun i _ ->
              let sb = sub #uint8 #len b (i * q) q in
              List.iter (fun a -> print_uint8_hex_pad a) (to_list sb);
              (if i < n - 1 then IO.print_string "\n"))
          ();
        (if r <> 0 then IO.print_newline ());
        let sb = sub #uint8 #len b (n * q) r in
        List.iter (fun a -> print_uint8_hex_pad a) (to_list sb)))
Lib.PrintSequence.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked
Lib.PrintSequence.fst
Prims.bool Lib.IntTypes.size_nat Lib.ByteSequence.lbytes Prims.op_Negation Prims.unit Prims.op_Equality Prims.int FStar.List.iter Lib.IntTypes.uint8 Lib.PrintSequence.print_uint8_hex_pad Lib.Sequence.to_list Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Sequence.lseq Lib.IntTypes.int_t Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.slice Prims.op_Multiply Prims.op_Addition Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThan Prims.l_or FStar.Seq.Base.index Lib.Sequence.index Lib.Sequence.sub FStar.Mul.op_Star Prims.op_disEquality FStar.IO.print_newline Lib.LoopCombinators.repeat_range_all_ml Prims.op_GreaterThanOrEqual Prims.op_Subtraction FStar.IO.print_string Prims.op_Modulus Prims.op_Division
module Lib.PrintSequence

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence
open Lib.LoopCombinators



let print_nat8_hex x =
  IO.print_uint8 (u8_to_UInt8 (u8 x))

let print_nat8_hex_pad x =
  IO.print_uint8_hex_pad (u8_to_UInt8 (u8 x))

let print_nat8_dec x =
  IO.print_uint8_dec (u8_to_UInt8 (u8 x))

let print_nat8_dec_pad x =
  IO.print_uint8_dec_pad (u8_to_UInt8 (u8 x))


let print_nat32_hex x =
  IO.print_uint32 (u32_to_UInt32 (u32 x))

let print_nat32_hex_pad x =
  IO.print_uint32_hex_pad (u32_to_UInt32 (u32 x))

let print_nat32_dec x =
  IO.print_uint32_dec (u32_to_UInt32 (u32 x))

let print_nat32_dec_pad x =
  IO.print_uint32_dec_pad (u32_to_UInt32 (u32 x))


let print_nat64_hex x =
  IO.print_uint64 (u64_to_UInt64 (u64 x))

let print_nat64_hex_pad x =
  IO.print_uint64_hex_pad (u64_to_UInt64 (u64 x))

let print_nat64_dec x =
  IO.print_uint64_dec (u64_to_UInt64 (u64 x))

let print_nat64_dec_pad x =
  IO.print_uint64_dec_pad (u64_to_UInt64 (u64 x))


let print_uint8_hex x =
  IO.print_uint8 (u8_to_UInt8 x)

let print_uint8_hex_pad x =
  IO.print_uint8_hex_pad (u8_to_UInt8 x)

let print_uint8_dec x =
  IO.print_uint8_dec (u8_to_UInt8 x)

let print_uint8_dec_pad x =
  IO.print_uint8_dec_pad (u8_to_UInt8 x)


let print_uint32_hex x =
  IO.print_uint32 (u32_to_UInt32 x)

let print_uint32_hex_pad x =
  IO.print_uint32_hex_pad (u32_to_UInt32 x)

let print_uint32_dec x =
  IO.print_uint32_dec (u32_to_UInt32 x)

let print_uint32_dec_pad x =
  IO.print_uint32_dec_pad (u32_to_UInt32 x)


let print_uint64_hex x =
  IO.print_uint64 (u64_to_UInt64 x)

let print_uint64_hex_pad x =
  IO.print_uint64_hex_pad (u64_to_UInt64 x)

let print_uint64_dec x =
  IO.print_uint64_dec (u64_to_UInt64 x)

let print_uint64_dec_pad x =
  IO.print_uint64_dec_pad (u64_to_UInt64 x)


let print_label_nat64 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_nat64_dec x;
  IO.print_string "\n")

let print_label_uint8 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint8_hex_pad x;
  IO.print_string "\n")

let print_label_uint32 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint32_hex_pad x;
  IO.print_string "\n")

let print_label_uint64 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint64_hex_pad x;
  IO.print_string "\n")


let print_list_nat64 flag l =
  if not flag then ()
  else (
  repeat_range_all_ml 0 (List.Tot.length l) (fun i _ ->
    print_nat64_dec (List.Tot.index l i);
    IO.print_string " "
  ) ())


let print_string flag s = if flag then IO.print_string s else ()
val print_lbytes: display:bool -> len:size_nat -> lbytes len -> FStar.All.ML unit
display: Prims.bool -> len: Lib.IntTypes.size_nat -> b: Lib.ByteSequence.lbytes len
  -> FStar.All.ML Prims.unit