val freevars_list (t: list term) : Set.set var
let rec freevars_list (t:list term) : Set.set var =
  match t with
  | [] -> Set.empty
  | hd::tl -> freevars hd `Set.union` freevars_list tl
val freevars_list (t: list term) : Set.set var
let rec freevars_list (t: list term) : Set.set var =
match t with
| [] -> Set.empty
| hd :: tl -> (freevars hd) `Set.union` (freevars_list tl)
Pulse.Syntax.Naming.fsti.checked
Pulse.Syntax.Pure.fst.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Common.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Pulse.Syntax.Naming.fsti
Prims.list Pulse.Syntax.Base.term FStar.Set.empty Pulse.Syntax.Base.var FStar.Set.union Pulse.Syntax.Naming.freevars Pulse.Syntax.Naming.freevars_list FStar.Set.set
module Pulse.Syntax.Naming

open FStar.List.Tot
open Pulse.Syntax.Base
open Pulse.Common

module L = FStar.List.Tot

module R = FStar.Reflection
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
module U = Pulse.Syntax.Pure
module E = Pulse.Elaborate.Pure

let rec freevars (t:term) 
  : Set.set var
  = match t.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames
    | Tm_EmpInames
    | Tm_Unknown -> Set.empty
    | Tm_Star t1 t2 ->
      Set.union (freevars t1) (freevars t2)
    | Tm_ExistsSL _ t1 t2
    | Tm_ForallSL _ t1 t2 ->
      Set.union (freevars t1.binder_ty) (freevars t2)
    | Tm_Pure p -> freevars p
    | Tm_FStar t -> RT.freevars t

let freevars_st_comp (s:st_comp) : Set.set var =
  freevars s.res `Set.union`
  freevars s.pre `Set.union`
  freevars s.post


let freevars_comp (c:comp) : Tot (Set.set var) (decreases c) =
  match c with
  | C_Tot t -> freevars t
  | C_ST s -> freevars_st_comp s
  | C_STAtomic inames s
  | C_STGhost inames s ->
    freevars inames `Set.union` freevars_st_comp s

let freevars_opt (f: 'a -> Set.set var) (x:option 'a) : Set.set var =
  match x with
  | None -> Set.empty
  | Some x -> f x

let freevars_term_opt (t:option term) : Set.set var =
  freevars_opt freevars t
val freevars_list (t: list term) : Set.set var
t: Prims.list Pulse.Syntax.Base.term -> FStar.Set.set Pulse.Syntax.Base.var