val aloc_domain
      (#al: aloc_t)
      (c: cls al)
      (regions: Ghost.erased (Set.set HS.rid))
      (addrs: (r: HS.rid{Set.mem r (Ghost.reveal regions)} -> GTot (GSet.set nat)))
    : GTot (GSet.set (aloc c))
let aloc_domain (#al: aloc_t) (c: cls al) (regions: Ghost.erased (Set.set HS.rid)) (addrs: ((r: HS.rid { Set.mem r (Ghost.reveal regions) } ) -> GTot (GSet.set nat))) : GTot (GSet.set (aloc c)) =
  GSet.comprehend (fun a -> Set.mem a.region (Ghost.reveal regions) && GSet.mem a.addr (addrs a.region))
val aloc_domain
      (#al: aloc_t)
      (c: cls al)
      (regions: Ghost.erased (Set.set HS.rid))
      (addrs: (r: HS.rid{Set.mem r (Ghost.reveal regions)} -> GTot (GSet.set nat)))
    : GTot (GSet.set (aloc c))
let aloc_domain
      (#al: aloc_t)
      (c: cls al)
      (regions: Ghost.erased (Set.set HS.rid))
      (addrs: (r: HS.rid{Set.mem r (Ghost.reveal regions)} -> GTot (GSet.set nat)))
    : GTot (GSet.set (aloc c)) =
GSet.comprehend (fun a ->
      Set.mem a.region (Ghost.reveal regions) && GSet.mem a.addr (addrs a.region))
FStar.ModifiesGen.fst.checked
prims.fst.checked FStar.Universe.fsti.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.SMT.fst.checked FStar.Tactics.Effect.fsti.checked FStar.StrongExcludedMiddle.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.GSet.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
FStar.ModifiesGen.fst
FStar.ModifiesGen.aloc_t FStar.ModifiesGen.cls FStar.Ghost.erased FStar.Set.set FStar.Monotonic.HyperHeap.rid Prims.b2t FStar.Set.mem FStar.Ghost.reveal FStar.GSet.set Prims.nat FStar.GSet.comprehend FStar.ModifiesGen.aloc Prims.op_AmpAmp FStar.ModifiesGen.__proj__ALoc__item__region FStar.GSet.mem FStar.ModifiesGen.__proj__ALoc__item__addr Prims.bool
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.ModifiesGen

#set-options "--split_queries no"
#set-options "--using_facts_from '*,-FStar.Tactics,-FStar.Reflection,-FStar.List'"

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

noeq
type aloc (#al: aloc_t) (c: cls al) = | ALoc:
  (region: HS.rid) ->
  (addr: nat) ->
  (loc: option (al region addr)) ->
  aloc c
val aloc_domain
      (#al: aloc_t)
      (c: cls al)
      (regions: Ghost.erased (Set.set HS.rid))
      (addrs: (r: HS.rid{Set.mem r (Ghost.reveal regions)} -> GTot (GSet.set nat)))
    : GTot (GSet.set (aloc c))

    c: FStar.ModifiesGen.cls al ->
    regions: FStar.Ghost.erased (FStar.Set.set FStar.Monotonic.HyperHeap.rid) ->
    addrs:
      (r: FStar.Monotonic.HyperHeap.rid{FStar.Set.mem r (FStar.Ghost.reveal regions)}
          -> Prims.GTot (FStar.GSet.set Prims.nat))
  -> Prims.GTot (FStar.GSet.set (FStar.ModifiesGen.aloc c))