let nonempty_field_description_t (t: Type0) =
  (fd: field_description_t t { fd.fd_empty == false })
let nonempty_field_description_t (t: Type0) =
(fd: field_description_t t {fd.fd_empty == false})
Steel.ST.C.Types.Fields.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Base.fsti.checked Steel.C.Typestring.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
Steel.ST.C.Types.Fields.fsti
Steel.ST.C.Types.Fields.field_description_t Prims.eq2 Prims.bool Steel.ST.C.Types.Fields.__proj__Mkfield_description_t__item__fd_empty
module Steel.ST.C.Types.Fields
include Steel.ST.C.Types.Base
open Steel.C.Typestring
open Steel.ST.Util

[@@noextract_to "krml"] // tactic
let norm_fields () : FStar.Tactics.Tac unit =
  FStar.Tactics.norm [delta_attr [`%norm_field_attr]; iota; zeta; primops];
  FStar.Tactics.trefl ()

[@@noextract_to "krml"] // primitive
val field_t_nil: Type0
[@@noextract_to "krml"] // primitive
val field_t_cons (fn: Type0) (ft: Type0) (fc: Type0): Type0

inline_for_extraction [@@noextract_to "krml"; norm_field_attr]
noeq
type field_description_t (t: Type0) : Type u#1 = {
  fd_def: (string -> GTot bool);
  fd_empty: (fd_empty: bool { fd_empty == true <==> (forall s . fd_def s == false) });
  fd_type: (string -> Type0);
  fd_typedef: ((s: string) -> Pure (typedef (fd_type s)) (requires (fd_def s)) (ensures (fun _ -> True)));
}

inline_for_extraction [@@noextract_to "krml"; norm_field_attr]
val nonempty_field_description_t : t: Type0 -> Type
t: Type0 -> Type