val set_def (#t: eqtype) (s: FStar.Set.set t) (x: t) : Tot bool
let set_def
  (#t: eqtype)
  (s: FStar.Set.set t)
  (x: t)
: Tot bool
= FStar.Set.mem x s
val set_def (#t: eqtype) (s: FStar.Set.set t) (x: t) : Tot bool
let set_def (#t: eqtype) (s: FStar.Set.set t) (x: t) : Tot bool =
FStar.Set.mem x s
Steel.ST.C.Types.UserStruct.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Struct.Aux.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.C.Types.UserStruct.fsti
Prims.eqtype FStar.Set.set FStar.Set.mem Prims.bool
module Steel.ST.C.Types.UserStruct
open Steel.ST.Util
open Steel.ST.C.Types.Struct.Aux

module Set = FStar.Set

(* This library allows the user to define their own struct type, with
a constructor from field values, and a destructor to field values for
each field. This may be necessary for recursive structs *)

let set_def
  (#t: eqtype)
  (s: FStar.Set.set t)
  (x: t)
val set_def (#t: eqtype) (s: FStar.Set.set t) (x: t) : Tot bool
s: FStar.Set.set t -> x: t -> Prims.bool