val always_valid: string -> Tot bool
let always_valid (_: string) : Tot bool = true
val always_valid: string -> Tot bool
let always_valid (_: string) : Tot bool =
true
Options.fst.checked
Version.fsti.checked prims.fst.checked OS.fsti.checked HashingOptions.fst.checked FStar.UInt8.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.Getopt.fsti.checked FStar.Char.fsti.checked FStar.All.fst.checked
Options.fst
Prims.string Prims.bool
module Options
open HashingOptions
open FStar.All
open FStar.ST
module U8 = FStar.UInt8
module OS = OS

#push-options "--warn_error -272" //top-level effects are okay

inline_for_extraction
let valid_string
  (valid: (string -> Tot bool))
: Tot Type0
= (s: string { valid s == true })
val always_valid: string -> Tot bool
_: Prims.string -> Prims.bool