val nat_t_of_nat (n: nat) : Type0
let rec nat_t_of_nat (n: nat): Type0 =
  match n with
  | 0 -> z
  | n -> s (nat_t_of_nat (n - 1))
val nat_t_of_nat (n: nat) : Type0
let rec nat_t_of_nat (n: nat) : Type0 =
match n with
| 0 -> z
| n -> s (nat_t_of_nat (n - 1))
Steel.C.Typenat.fsti.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
Steel.C.Typenat.fsti
Prims.nat Steel.C.Typenat.z Prims.int Steel.C.Typenat.s Steel.C.Typenat.nat_t_of_nat Prims.op_Subtraction
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
val nat_t_of_nat (n: nat) : Type0
n: Prims.nat -> Type0