Standard constructive definitions of integers, rationals, and reals?

Natural numbers are defined inductively as (using Coq syntax as an example)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Is there a standard way to define integers (and maybe other sets like rationals and reals) constructively?

Gilles answer is a good one, except for the paragraph on the real numbers, which is completely false, except for the fact that the real numbers are indeed a different kettle of fish. Because this sort of misinformation seems to be quite widespread, I would like to record here a detailed rebuttal.

It is not true that all inductive types are denumerable. For example, the inductive type

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

is not denumerable, for given any sequence c : nat -> cow we may form horn c which is not in the sequence by well-foundedness of cattle. If you want a correct statement of the form "all inductive types are countable" you have to severely limit the allowed constructions.

The real numbers cannot be easily constructed as an inductive type, except that in homotopy type theory they can be constructed as a higher inductive-inductive type, see Chapter 11 of the HoTT book. It could be argued that this is cheating.

There are a number of constructive definitions and constructions of the reals, contrary to Gilles claim. They can be broadly divided into two classes:

-
Cauchy-type constructions in which the reals as seen as a metric completion of the rational numbers. This sort of construction often requires quotients, although one may be able to get away with a coiunductive definition, dependig on how one treats equality. A naive construction typically requires countable choice as well, but Fred Richman gave a completion procedure which works constructively without choice, see his Real numbers and other completions.

-
Dedekind-type construction in which the reals are seen as (two-sided) cuts of rationals. This sort of construction usually requires powersets or a similar device, although it is possible to do it just with some basic $\lambda$-calculus and the axiomatization of the Sierpinski space $\Sigma$, see Dedekind reals in Abstract Stone Duality.

On the implementation side, we have various constructive formalizations of reals (but not the one in the Coq standard library which is just awful), for instance Robbert Krebbers's and Bas Spitters's Computer certified efficient exact reals in Coq.

For an actual implementation of exact real numbers I point you to Norbert Müller's iRRAM.

Lastly, Gilles remark about denumerable subsets of reals is off the mark. It is perfectly possible to construct or define uncountable sets, in whatever constructive setting you live. For example, the Baire space $\mathbb{N} \to \mathbb{N}$ of all sequences of numbers is alway uncountable, even if you think that every function is Turing-computable -- see my blog post for an explanation.

StackExchange Computer Science Q#40479, answer score: 16