val set_snoc (#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))))
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
val set_snoc (#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))))
let set_snoc (#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)
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.union FStar.Set.singleton Steel.ST.C.Types.UserStruct.nonempty_set Prims.l_True Prims.l_Forall Prims.eq2 Prims.bool FStar.Set.mem Prims.op_BarBar Prims.op_Equality
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))
val set_snoc (#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.set t -> a: t -> Prims.Pure (Steel.ST.C.Types.UserStruct.nonempty_set t)