val field_t (s: Set.set string) : Tot eqtype
let field_t (s: Set.set string) : Tot eqtype =
  (f: string { Set.mem f s })
val field_t (s: Set.set string) : Tot eqtype
let field_t (s: Set.set string) : Tot eqtype =
(f: string{Set.mem f 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
FStar.Set.set Prims.string Prims.b2t FStar.Set.mem Prims.eqtype
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)
: Tot bool
= FStar.Set.mem x s

noextract
let nonempty_set (t: eqtype) =
  (s: Set.set t { exists x . set_def s x == true })

noextract
let set_snoc // for associativity reasons
(#t: eqtype) (q: FStar.Set.set t) (a: t) : Pure (nonempty_set t)
  (requires True)
  (ensures (fun s ->
    (forall (x: t). {:pattern FStar.Set.mem x s} FStar.Set.mem x s == (x = a || FStar.Set.mem x q))
  ))
= q `FStar.Set.union` FStar.Set.singleton a

[@@noextract_to "krml"]
val field_t (s: Set.set string) : Tot eqtype
s: FStar.Set.set Prims.string -> Prims.eqtype