let elab_frame (c:comp_st) (frame:term) (e:R.term) =
  let u = comp_u c in
  let ty = elab_term (comp_res c) in
  let pre = elab_term (comp_pre c) in
  let post = elab_term (comp_post c) in
  if C_ST? c
  then mk_frame_stt u ty pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
  else let opened = elab_term (comp_inames c) in      
       if C_STAtomic? c
       then mk_frame_stt_atomic u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
       else let _ = assert (C_STGhost? c) in
            mk_frame_stt_ghost u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
let elab_frame (c: comp_st) (frame: term) (e: R.term) =
let u = comp_u c in
let ty = elab_term (comp_res c) in
let pre = elab_term (comp_pre c) in
let post = elab_term (comp_post c) in
if C_ST? c
then mk_frame_stt u ty pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
else
  let opened = elab_term (comp_inames c) in
  if C_STAtomic? c
  then mk_frame_stt_atomic u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
  else
    let _ = assert (C_STGhost? c) in
    mk_frame_stt_ghost u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
Pulse.Elaborate.Core.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.Pure.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Elaborate.Core.fst
Pulse.Syntax.Base.comp_st Pulse.Syntax.Base.term FStar.Reflection.Types.term Pulse.Syntax.Base.uu___is_C_ST Pulse.Reflection.Util.mk_frame_stt Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Pulse.Elaborate.Pure.elab_term Prims.bool Pulse.Syntax.Base.uu___is_C_STAtomic Pulse.Reflection.Util.mk_frame_stt_atomic Pulse.Reflection.Util.mk_frame_stt_ghost Prims.unit Prims._assert Prims.b2t Pulse.Syntax.Base.uu___is_C_STGhost Pulse.Syntax.Base.comp_inames Pulse.Syntax.Base.comp_post Pulse.Syntax.Base.comp_pre Pulse.Syntax.Base.comp_res Pulse.Syntax.Base.universe Pulse.Syntax.Base.comp_u
module Pulse.Elaborate.Core
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Elaborate.Pure
open Pulse.Typing

open Pulse.Reflection.Util
val elab_frame : c: Pulse.Syntax.Base.comp_st -> frame: Pulse.Syntax.Base.term -> e: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term
c: Pulse.Syntax.Base.comp_st -> frame: Pulse.Syntax.Base.term -> e: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term