Now that you have multiplication for nat_nums, you can define a factorial function for nat_nums. Call your function facty_nn. It should take a nat_num as its input and generate the factorial of that nat_num (as a nat_num) as its output, as illustrated below: # facty_nn (S(S(S(Z))));; - : nat_num = S (S (S (S (S (S Z))))) # nat_num_to_num (facty_nn (num_to_nat_num 5));; - : int = 120