coq. ordered pair of natual numbers

Question

I am trying to defined an inductive data type to hold pair of natural numbers. Here is what I have done

   Definition ordered_pair := (nat * nat) % type.

   Inductive nat_pair(A B:nat):ordered_pair:=
     |pair :ordered_pair->ordered_pair.

It generates exception

   Anomaly: Uncaught exception Reduction.NotArity. Please report.

Does anyone know there?

Answer 1

This inductive definition just does not make sense.

The type ordered_pair you have defined is already a type for pairs of natural numbers. It is defined as the pair type, applied to arguments of type nat, so to build such a pair you could do:

Definition p : ordered_pair := (23, 42).

Now if you wanted to define a "similar" (but not "identical") type inductively, the syntax would be:

Inductive nat_pair : Set :=
| pair : nat -> nat -> nat_pair
.

Notice that you don't take natural numbers as parameters in the type, but rather the constructor contains two such numbers.

You seem to have some misunderstanding of inductive definitions, so I'd suggest reading more about them.