Search code examples
coq

Using tuples when constructing inductive types

I'm trying to use a pair to pass as an argument into an inductive type in Coq

Definition pair := (nat,nat).

Inductive use_pair :=
  | mktriplet : pair -> nat -> use_pair.

However, this gives the error:

Error: In environment
use_pair : Type
The term "pair" has type "(Set * Set)%type"
which should be Set, Prop or Type.

I can get this to work

Inductive use_pair :=
  | mktriplet : (Set * Set) -> nat -> use_pair.

But I would like to specify that the only tuple which will work is (nat,nat).

How can I specify this? I see the notation scope %type but that seems different than Type, though I don't know how to experiment with this; Check type returns an error.

Solution

  • Did you mean to do this?

    Definition pair : Type := nat * nat.

Inductive use_pair :=
  | mktriplet : pair -> nat -> use_pair.