val canon_comp (c: comp_st) : comp_st
let canon_comp (c:comp_st) : comp_st = 
  match readback_comp (elab_comp c) with
  | None -> c
  | Some (C_Tot _) -> c //should be impossible
  | Some c' -> c'
val canon_comp (c: comp_st) : comp_st
let canon_comp (c: comp_st) : comp_st =
match readback_comp (elab_comp c) with
| None -> c
| Some (C_Tot _) -> c
| Some c' -> c'
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.Syntax.Base.comp_st Pulse.Readback.readback_comp Pulse.Elaborate.Pure.elab_comp Pulse.Syntax.Base.term Pulse.Syntax.Base.comp Prims.eq2 FStar.Reflection.Types.term
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

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 canon_comp (c: comp_st) : comp_st
c: Pulse.Syntax.Base.comp_st -> Pulse.Syntax.Base.comp_st