let norm_typenat =
  [
    delta_only [
      `%nat_t_of_nat;
    ];
    iota; zeta; primops;
  ]
let norm_typenat =
[delta_only [`%nat_t_of_nat]; iota; zeta; primops]
Steel.C.Typenat.fsti.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
Steel.C.Typenat.fsti
Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta_only Prims.string Prims.Nil FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.primops
module Steel.C.Typenat

(** Suppose [array (n : nat) (t : Type)] represents the type of array values.
    Then, when extracting values of type [ref (array n t)], the length n is lost.
    To make sure this information sticks around, this module provides
    an encoding of natural numbers as types. *)

val z: Type0
val s: Type0 -> Type0

let rec nat_t_of_nat (n: nat): Type0 =
  match n with
  | 0 -> z
  | n -> s (nat_t_of_nat (n - 1))

unfold
val norm_typenat : Prims.list FStar.Pervasives.norm_step
Prims.list FStar.Pervasives.norm_step