val norm_fields: Prims.unit -> FStar.Tactics.Tac unit
let norm_fields () : FStar.Tactics.Tac unit =
  FStar.Tactics.norm [delta_attr [`%norm_field_attr]; iota; zeta; primops];
  FStar.Tactics.trefl ()
val norm_fields: Prims.unit -> FStar.Tactics.Tac unit
let norm_fields () : FStar.Tactics.Tac unit =
FStar.Tactics.norm [delta_attr [`%norm_field_attr]; iota; zeta; primops];
FStar.Tactics.trefl ()
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
Prims.unit FStar.Tactics.V1.Derived.trefl FStar.Tactics.V1.Builtins.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta_attr Prims.string Prims.Nil FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.primops
module Steel.ST.C.Types.Fields
include Steel.ST.C.Types.Base
open Steel.C.Typestring
open Steel.ST.Util

[@@noextract_to "krml"] // tactic
val norm_fields: Prims.unit -> FStar.Tactics.Tac unit
_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit