val print : s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
let print s = discard (IO.debug_print_string ("RNG| "^s^"\n"))
module MiTLS.Random
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError

val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked EverCrypt.AutoConfig2.fsti.checked
MiTLS.Random.fst
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
Prims.string MiTLS.Random.discard FStar.IO.debug_print_string Prims.op_Hat Prims.unit
let print s =
  
discard (IO.debug_print_string ("RNG| " ^ s ^ "\n"))