Partial functions abound in modern computing theory, and so any system which purports to naturally formalize it must treat them. Surprisingly, the most common treatments do not work well for constructive formal systems, i.e., for those with computational content. Since constructive formal systems are significant in computer science, it is important to give an account of partial functions in them. This paper does that by construing a partial function $\phi :N \rightarrow N$ as a total function $f:D_{f}\rightarrow N$ for $D_{f}$ an inductively defined set generated simultaneously with $f$. This idea has appeared in other guises, at least in the author's previous work, but here it is presented in a pure form. It is compared to Scott's method of using total functions on domains. A formal system of arithmetic is defined to illustrate the ideas. The system is shown consistent relative to constructive type theory; from this result important corollaries are drawn about using the theory as a programming language. KEY WORDS AND PHRASES: automated logic, Heyting arithmetic, constructivity, intuitionistic predicate calculus, partial functions, recursive functions, programming logics, program verification, type theory, type checking.