val st_comp_with_pre (st: st_comp) (pre: term) : st_comp
let st_comp_with_pre (st:st_comp) (pre:term) : st_comp = { st with pre }
val st_comp_with_pre (st: st_comp) (pre: term) : st_comp
let st_comp_with_pre (st: st_comp) (pre: term) : st_comp =
{ st with pre = pre }
Pulse.Typing.Combinators.fsti.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Typing.Combinators.fsti
Pulse.Syntax.Base.st_comp Pulse.Syntax.Base.term Pulse.Syntax.Base.Mkst_comp Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Syntax.Base.__proj__Mkst_comp__item__res Pulse.Syntax.Base.__proj__Mkst_comp__item__post
module Pulse.Typing.Combinators

module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
val st_comp_with_pre (st: st_comp) (pre: term) : st_comp
st: Pulse.Syntax.Base.st_comp -> pre: Pulse.Syntax.Base.term -> Pulse.Syntax.Base.st_comp