val nvar_as_binder (x: nvar) (t: term) : binder
let nvar_as_binder (x:nvar) (t:term) : binder =
  {binder_ty=t;binder_ppname=fst x}
val nvar_as_binder (x: nvar) (t: term) : binder
let nvar_as_binder (x: nvar) (t: term) : binder =
{ binder_ty = t; binder_ppname = fst x }
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.nvar Pulse.Syntax.Base.term Pulse.Syntax.Base.Mkbinder FStar.Pervasives.Native.fst Pulse.Syntax.Base.ppname Pulse.Syntax.Base.var Pulse.Syntax.Base.binder
module Pulse.Typing.Combinators

module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing

let st_comp_with_pre (st:st_comp) (pre:term) : st_comp = { st with pre }
val nvar_as_binder (x: nvar) (t: term) : binder
x: Pulse.Syntax.Base.nvar -> t: Pulse.Syntax.Base.term -> Pulse.Syntax.Base.binder