val get_non_space (x: list char) : 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 get_non_space (x: list char) : 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]
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
Prims.list FStar.String.char Prims.op_Equality FStar.Char.char Vale.Transformers.DebugPrint.get_non_space Prims.bool FStar.String.string_of_list Prims.Cons Prims.Nil 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
val get_non_space (x: list char) : string
x: Prims.list FStar.String.char -> Prims.string