val print_separation: Prims.unit -> ML unit
val print_separation: Prims.unit -> ML unit
let print_separation () : ML unit = IO.print_string "==================\n\n"
(* TODO: I would like to change the name of the module (remove the 'Spec')
 * but then we need to create a special build rule in the Makefile, because
 * otherwise no .ml file is generated (and thus the tests can't be run). *)
module Spec.Noise.Utils

open Spec.Noise

open FStar.All
module IO = FStar.IO
module List = FStar.List

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence
/
Spec.Noise.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Noise.Utils.fst
_: Prims.unit -> FStar.All.ML Prims.unit
Prims.unit FStar.IO.print_string
let print_separation () : ML unit =
  
IO.print_string "==================\n\n"