let print_ins i _ =
  get_non_space (list_of_string (print_ins i gcc))
let print_ins i _ =
get_non_space (list_of_string (print_ins i gcc))
Vale.Transformers.DebugPrint.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Char.fsti.checked
Vale.Transformers.DebugPrint.fst
Vale.X64.Machine_Semantics_s.ins Vale.Transformers.DebugPrint.get_non_space FStar.String.list_of_string Vale.X64.Print_s.print_ins Vale.X64.Print_s.gcc Prims.string
(**

   This is a convenience module for making it easier to debug
   transformations by overriding some printers. You probably do not want
   to use this module unless you know exactly what you're doing.

*)
module Vale.Transformers.DebugPrint

open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.Def.PossiblyMonad
open Vale.X64.Decls
open Vale.X64.Print_s
open FStar.String

let rec get_non_space (x:list char) : string =
  match x with
  | [] -> "."
  | x :: xs ->
    if x = ' ' then get_non_space xs else string_of_list [x]
val print_ins : i: Vale.X64.Machine_Semantics_s.ins -> _: _ -> Prims.string
i: Vale.X64.Machine_Semantics_s.ins -> _: _ -> Prims.string