val debug_flag : string -> Tac bool
let debug_flag (s:string) : Tac bool =
  let v = ext_getv ("pulse:" ^ s) in
  v <> "" && v <> "0" && v <> "false"
val debug_flag : string -> Tac bool
let debug_flag (s: string) : Tac bool =
let v = ext_getv ("pulse:" ^ s) in
v <> "" && v <> "0" && v <> "false"
Pulse.Config.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked
Pulse.Config.fst
Prims.string Prims.op_AmpAmp Prims.op_disEquality Prims.bool FStar.Tactics.V2.Builtins.ext_getv Prims.op_Hat
module Pulse.Config

open FStar.Tactics.V2

(* This is currently unused, we use the --ext option instead. *)
let join_goals : bool = false
val debug_flag : string -> Tac bool
s: Prims.string -> FStar.Tactics.Effect.Tac Prims.bool