ComFreek/convert-nat-to-string-in-coq.md

## convert-nat-to-string-in-coq.md

      
    Raw
  

              convert-nat-to-string-in-coq.md
            
          
    Every time I wanted to convert nat to string in the most obvious manner (i.e. decimal), I had to search >= 10min in the libraries for the right function calls!
Require Import Numbers.DecimalString.
Require Import Numbers.DecimalNat.

Definition nat_to_string (n: nat) := NilZero.string_of_uint (Decimal.rev (Unsigned.to_lu n)).
Compute (nat_to_string 0).   (*  "0" *)
Compute (nat_to_string 42).  (* "42" *)