let vars_of_rt_env (g:R.env) = Set.intension (fun x -> Some? (RT.lookup_bvar g x))
let vars_of_rt_env (g: R.env) =
Set.intension (fun x -> Some? (RT.lookup_bvar g x))
Pulse.Typing.FV.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.Common.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Set.fsti.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 FStar.Calc.fsti.checked
Pulse.Typing.FV.fst
FStar.Reflection.Types.env FStar.Set.intension Prims.int FStar.Pervasives.Native.uu___is_Some FStar.Reflection.Types.term FStar.Reflection.Typing.lookup_bvar Prims.bool FStar.Set.set
module Pulse.Typing.FV
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
open Pulse.Elaborate
open Pulse.Soundness.Common
val vars_of_rt_env : g: FStar.Reflection.Types.env -> Prims.GTot (FStar.Set.set Prims.int)
g: FStar.Reflection.Types.env -> Prims.GTot (FStar.Set.set Prims.int)