val debug_log (f: (unit -> T.Tac unit)) : T.Tac unit
let debug_log (f: unit -> T.Tac unit) : T.Tac unit = if RU.debug_at_level_no_module "readback" then f()
val debug_log (f: (unit -> T.Tac unit)) : T.Tac unit
let debug_log (f: (unit -> T.Tac unit)) : T.Tac unit =
if RU.debug_at_level_no_module "readback" then f ()
Pulse.Readback.fst.checked
Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Readback.fst
Prims.unit Pulse.RuntimeUtils.debug_at_level_no_module Prims.bool
module Pulse.Readback
module R = FStar.Reflection.V2
open Pulse.Syntax.Base
open Pulse.Reflection.Util
module RU = Pulse.RuntimeUtils
module T = FStar.Tactics
val debug_log (f: (unit -> T.Tac unit)) : T.Tac unit
f: (_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit) -> FStar.Tactics.Effect.Tac Prims.unit