val open_write_file (s: string) : ML FStar.IO.fd_write
let open_write_file (s:string) : ML FStar.IO.fd_write =
  FStar.IO.print_string (FStar.Printf.sprintf "Writing file %s\n" s);
  FStar.IO.open_write_file s
val open_write_file (s: string) : ML FStar.IO.fd_write
let open_write_file (s: string) : ML FStar.IO.fd_write =
FStar.IO.print_string (FStar.Printf.sprintf "Writing file %s\n" s);
FStar.IO.open_write_file s
Main.fst.checked
Z3TestGen.fst.checked Z3.fsti.checked TypeSizes.fsti.checked TranslateForInterpreter.fsti.checked Target.fsti.checked StaticAssertions.fst.checked Simplify.fsti.checked prims.fst.checked ParserDriver.fsti.checked OS.fsti.checked Options.fsti.checked JSON.fsti.checked InterpreterTarget.fsti.checked InlineSingletonRecords.fst.checked HashingOptions.fst.checked GenMakefile.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Desugar.fst.checked Deps.fsti.checked Config.fst.checked BitFields.fst.checked Binding.fsti.checked Batch.fsti.checked Ast.fst.checked
Main.fst
Prims.string FStar.IO.open_write_file FStar.IO.fd_write Prims.unit FStar.IO.print_string FStar.Printf.sprintf
module Main
open FStar.IO
open FStar.All
open Ast
open ParserDriver
module T = Target
open FStar.ST
#push-options "--z3rlimit_factor 2"
val open_write_file (s: string) : ML FStar.IO.fd_write
s: Prims.string -> FStar.All.ML FStar.IO.fd_write