val starts_with_capital (s: string) : Tot bool
let starts_with_capital (s: string) : Tot bool =
  String.length s >= 1 &&
  begin let first = String.sub s 0 1 in
    String.compare first "A" >= 0 && String.compare first "Z" <= 0
  end
val starts_with_capital (s: string) : Tot bool
let starts_with_capital (s: string) : Tot bool =
String.length s >= 1 &&
(let first = String.sub s 0 1 in
  String.compare first "A" >= 0 && String.compare first "Z" <= 0)
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.op_AmpAmp Prims.op_GreaterThanOrEqual FStar.String.length FStar.String.compare Prims.op_LessThanOrEqual Prims.b2t Prims.op_Equality Prims.nat FStar.String.strlen FStar.String.sub 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 })

let always_valid (_: string) : Tot bool = true
val starts_with_capital (s: string) : Tot bool
s: Prims.string -> Prims.bool