val 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
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_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
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
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 Prims.squash FStar.Pervasives.norm Steel.C.Typestring.norm_typestring Prims.eq2 Steel.C.Typestring.mk_string_t Steel.ST.C.Types.Fields.nonempty_field_description_t Steel.ST.C.Types.Struct.struct_t0
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"]
val 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
n: Prims.string -> fields: Steel.ST.C.Types.Fields.nonempty_field_description_t tf -> Type0