This question is an exact duplicate of:
People usually say Coq does not allow writing non-terminating functions. I have a question regarding that.
Does Coq allow writing exactly all terminating functions? In other words, what are the completeness and soundness properties of Coq's procedure for checking well-foundness of fixpoint definitions?