let debug (g:env) (msg: unit -> T.Tac string) =
  let tac_debugging = T.debugging () in
  if tac_debugging || RU.debug_at_level (fstar_env g) "refl_tc_callbacks"
  then T.print (print_context g ^ "\n" ^ msg())
let debug (g: env) (msg: (unit -> T.Tac string)) =
let tac_debugging = T.debugging () in
if tac_debugging || RU.debug_at_level (fstar_env g) "refl_tc_callbacks"
then T.print (print_context g ^ "\n" ^ msg ())
Pulse.Checker.Pure.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked Pulse.PP.fst.checked prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.Squash.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Issue.fsti.checked
Pulse.Checker.Pure.fst
Pulse.Typing.Env.env Prims.unit Prims.string Prims.op_BarBar Pulse.RuntimeUtils.debug_at_level Pulse.Typing.Env.fstar_env FStar.Tactics.V2.Builtins.print Prims.op_Hat Pulse.Typing.Env.print_context Prims.bool FStar.Tactics.V2.Builtins.debugging
module Pulse.Checker.Pure
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.Tactics.V2
open FStar.Reflection.V2 (* shadow named view *)

open Pulse.Reflection
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
module P = Pulse.Syntax.Printer
module RTB = FStar.Tactics.V2.Builtins
module RU = Pulse.RuntimeUtils
val debug : g: Pulse.Typing.Env.env -> msg: (_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.string)
  -> FStar.Tactics.Effect.Tac Prims.unit
g: Pulse.Typing.Env.env -> msg: (_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.string)
  -> FStar.Tactics.Effect.Tac Prims.unit