val debug_log (g: env) (f: (unit -> T.Tac unit)) : T.Tac unit
let debug_log (g:env) (f:unit -> T.Tac unit) : T.Tac unit = if RU.debug_at_level (fstar_env g) "st_app" then f () else ()
val debug_log (g: env) (f: (unit -> T.Tac unit)) : T.Tac unit
let debug_log (g: env) (f: (unit -> T.Tac unit)) : T.Tac unit =
if RU.debug_at_level (fstar_env g) "st_app" then f ()
Pulse.Checker.STApp.fst.checked
Pulse.Typing.FV.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.STApp.fst
Pulse.Typing.Env.env Prims.unit Pulse.RuntimeUtils.debug_at_level Pulse.Typing.Env.fstar_env Prims.bool
module Pulse.Checker.STApp

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure
open Pulse.Checker.Base

module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module FV = Pulse.Typing.FV
module RU = Pulse.RuntimeUtils
module P = Pulse.Syntax.Printer
module Prover = Pulse.Checker.Prover
val debug_log (g: env) (f: (unit -> T.Tac unit)) : T.Tac unit
g: Pulse.Typing.Env.env -> f: (_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit)
  -> FStar.Tactics.Effect.Tac Prims.unit