val push_context (ctx: string) (r: range) (g: env) : (g': env{g == g'})
let push_context (ctx:string) (r:range) (g:env) : (g':env { g == g' })
  = push_context g ctx r
val push_context (ctx: string) (r: range) (g: env) : (g': env{g == g'})
let push_context (ctx: string) (r: range) (g: env) : (g': env{g == g'}) =
push_context g ctx r
Pulse.Checker.Pure.fsti.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Readback.fsti.checked Pulse.Elaborate.Pure.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Builtins.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Pure.fsti
Prims.string Pulse.Syntax.Base.range Pulse.Typing.Env.env Pulse.Typing.Env.push_context Prims.eq2
module Pulse.Checker.Pure
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.Readback
module RTB = FStar.Tactics.Builtins
module RU = Pulse.RuntimeUtils
val push_context (ctx: string) (r: range) (g: env) : (g': env{g == g'})
ctx: Prims.string -> r: Pulse.Syntax.Base.range -> g: Pulse.Typing.Env.env
  -> g': Pulse.Typing.Env.env{g == g'}