This paper provides an explicit description of a model for intuitionistic non-standard arithmetic, which can be formalized in a constructive metatheory without the axiom of choice.