val struct_get_field_pat
      (#tn #tf: Type0)
      (#n: string)
      (#fields: nonempty_field_description_t tf)
      (s: struct_t0 tn n fields)
      (field: field_t fields)
      (v: fields.fd_type field)
      (field': field_t fields)
    : Lemma
      (struct_get_field (struct_set_field field v s) field' ==
        (if field' = field then v else struct_get_field s field'))
      [SMTPat (struct_get_field (struct_set_field field v s) field')]
let struct_get_field_pat
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s: struct_t0 tn n fields)
  (field: field_t fields)
  (v: fields.fd_type field)
  (field': field_t fields)
: Lemma
  (struct_get_field (struct_set_field field v s) field' == (if field' = field then v else struct_get_field s field'))
  [SMTPat (struct_get_field (struct_set_field field v s) field')]
= if field' = field
  then ()
  else struct_get_field_other s field v field'
val struct_get_field_pat
      (#tn #tf: Type0)
      (#n: string)
      (#fields: nonempty_field_description_t tf)
      (s: struct_t0 tn n fields)
      (field: field_t fields)
      (v: fields.fd_type field)
      (field': field_t fields)
    : Lemma
      (struct_get_field (struct_set_field field v s) field' ==
        (if field' = field then v else struct_get_field s field'))
      [SMTPat (struct_get_field (struct_set_field field v s) field')]
let struct_get_field_pat
      (#tn #tf: Type0)
      (#n: string)
      (#fields: nonempty_field_description_t tf)
      (s: struct_t0 tn n fields)
      (field: field_t fields)
      (v: fields.fd_type field)
      (field': field_t fields)
    : Lemma
      (struct_get_field (struct_set_field field v s) field' ==
        (if field' = field then v else struct_get_field s field'))
      [SMTPat (struct_get_field (struct_set_field field v s) field')] =
if field' = field then () else struct_get_field_other s field v field'
Steel.ST.C.Types.Struct.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Fields.fsti.checked Steel.FractionalPermission.fst.checked Steel.C.Typestring.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.C.Types.Struct.fsti
Prims.string Steel.ST.C.Types.Fields.nonempty_field_description_t Steel.ST.C.Types.Struct.struct_t0 Steel.ST.C.Types.Fields.field_t Steel.ST.C.Types.Fields.__proj__Mkfield_description_t__item__fd_type Prims.op_Equality Prims.bool Steel.ST.C.Types.Struct.struct_get_field_other Prims.unit Prims.l_True Prims.squash Prims.eq2 Steel.ST.C.Types.Struct.struct_get_field Steel.ST.C.Types.Struct.struct_set_field Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module Steel.ST.C.Types.Struct
open Steel.ST.Util
include Steel.ST.C.Types.Fields
open Steel.C.Typestring

module P = Steel.FractionalPermission

// To be extracted as: struct t { fields ... }

[@@noextract_to "krml"] // primitive
val define_struct0 (tn: Type0) (#tf: Type0) (n: string) (fields: nonempty_field_description_t tf) : Tot Type0
inline_for_extraction [@@noextract_to "krml"]
let define_struct (n: string) (#tf: Type0) (#tn: Type0) (#[solve_mk_string_t ()] prf: squash (norm norm_typestring (mk_string_t n == tn))) (fields: nonempty_field_description_t tf) : Tot Type0
= define_struct0 tn #tf n fields

// To be extracted as: struct t
[@@noextract_to "krml"] // primitive
val struct_t0 (tn: Type0) (#tf: Type0) (n: string) (fields: nonempty_field_description_t tf) : Tot Type0
inline_for_extraction [@@noextract_to "krml"]
let struct_t (#tf: Type0) (n: string) (#tn: Type0) (# [solve_mk_string_t ()] prf: squash (norm norm_typestring (mk_string_t n == tn))) (fields: nonempty_field_description_t tf) : Tot Type0
= struct_t0 tn #tf n fields

val struct_set_field (#tn: Type0) (#tf: Type0) (#n: string) (#fields: nonempty_field_description_t tf) (f: field_t fields) (v: fields.fd_type f) (s: struct_t0 tn n fields) : GTot (struct_t0 tn n fields)

val struct_get_field
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s: struct_t0 tn n fields)
  (field: field_t fields)
: GTot (fields.fd_type field)

val struct_eq
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s1 s2: struct_t0 tn n fields)
: Ghost prop
  (requires True)
  (ensures (fun y ->
    (y <==> (s1 == s2)) /\
    (y <==> (forall field . struct_get_field s1 field == struct_get_field s2 field))
  ))

val struct_get_field_same
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s: struct_t0 tn n fields)
  (field: field_t fields)
  (v: fields.fd_type field)
: Lemma
  (struct_get_field (struct_set_field field v s) field == v)
  [SMTPat (struct_get_field (struct_set_field field v s) field)]

val struct_get_field_other
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s: struct_t0 tn n fields)
  (field: field_t fields)
  (v: fields.fd_type field)
  (field': field_t fields)
: Lemma
  (requires (field' <> field))
  (ensures (struct_get_field (struct_set_field field v s) field' == struct_get_field s field'))

let struct_get_field_pat
  (#tn: Type0)
  (#tf: Type0)
  (#n: string)
  (#fields: nonempty_field_description_t tf)
  (s: struct_t0 tn n fields)
  (field: field_t fields)
  (v: fields.fd_type field)
  (field': field_t fields)
: Lemma
  (struct_get_field (struct_set_field field v s) field' == (if field' = field then v else struct_get_field s field'))
val struct_get_field_pat
      (#tn #tf: Type0)
      (#n: string)
      (#fields: nonempty_field_description_t tf)
      (s: struct_t0 tn n fields)
      (field: field_t fields)
      (v: fields.fd_type field)
      (field': field_t fields)
    : Lemma
      (struct_get_field (struct_set_field field v s) field' ==
        (if field' = field then v else struct_get_field s field'))
      [SMTPat (struct_get_field (struct_set_field field v s) field')]

    s: Steel.ST.C.Types.Struct.struct_t0 tn n fields ->
    field: Steel.ST.C.Types.Fields.field_t fields ->
    v: Mkfield_description_t?.fd_type fields field ->
    field': Steel.ST.C.Types.Fields.field_t fields
  -> FStar.Pervasives.Lemma
      (ensures
        Steel.ST.C.Types.Struct.struct_get_field (Steel.ST.C.Types.Struct.struct_set_field field v s
          )
          field' ==
        (match field' = field with
          | true -> v
          | _ -> Steel.ST.C.Types.Struct.struct_get_field s field'))
      [
        SMTPat (Steel.ST.C.Types.Struct.struct_get_field (Steel.ST.C.Types.Struct.struct_set_field field
                  v
                  s)
              field')
      ]