val nonempty_set_nonempty_type (x: string) (s: Set.set string)
    : Lemma (requires (x `Set.mem` s)) (ensures (exists (x: field_t s). True))
let nonempty_set_nonempty_type (x: string) (s: Set.set string) : Lemma
  (requires (x `Set.mem` s))
  (ensures (exists (x: field_t s) . True))
= Classical.exists_intro (fun (_: field_t s) -> True) x
val nonempty_set_nonempty_type (x: string) (s: Set.set string)
    : Lemma (requires (x `Set.mem` s)) (ensures (exists (x: field_t s). True))
let nonempty_set_nonempty_type (x: string) (s: Set.set string)
    : Lemma (requires (x `Set.mem` s)) (ensures (exists (x: field_t s). True)) =
Classical.exists_intro (fun (_: field_t s) -> True) x
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.string FStar.Set.set FStar.Classical.exists_intro Steel.ST.C.Types.UserStruct.field_t Prims.l_True Prims.unit Prims.b2t FStar.Set.mem Prims.squash Prims.l_Exists Prims.Nil FStar.Pervasives.pattern
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"]
let field_t (s: Set.set string) : Tot eqtype =
  (f: string { Set.mem f s })

[@@noextract_to "krml"; norm_field_attr]
inline_for_extraction // for field_desc.fd_type
noeq
type struct_def (t: Type) = {
  fields: Set.set string;
  field_desc: field_description_gen_t (field_t fields);
  mk: ((f: field_t fields) -> Tot (field_desc.fd_type f)) -> Tot t;
  get: (t -> (f: field_t fields) -> Tot (field_desc.fd_type f));
  get_mk: (phi: ((f: field_t fields) -> Tot (field_desc.fd_type f))) -> (f: field_t fields) -> Lemma
    (get (mk phi) f == phi f);
  extensionality: (x1: t) -> (x2: t) -> ((f: field_t fields) -> Lemma (get x1 f == get x2 f)) -> Lemma (x1 == x2);
}

let nonempty_set_nonempty_type (x: string) (s: Set.set string) : Lemma
  (requires (x `Set.mem` s))
val nonempty_set_nonempty_type (x: string) (s: Set.set string)
    : Lemma (requires (x `Set.mem` s)) (ensures (exists (x: field_t s). True))
x: Prims.string -> s: FStar.Set.set Prims.string
  -> FStar.Pervasives.Lemma (requires FStar.Set.mem x s)
      (ensures exists (x: Steel.ST.C.Types.UserStruct.field_t s). Prims.l_True)