Search code examples
coq

Coq constructor can't take two arguments of different types?

I am just getting started with Coq and am confused as to why this isn't allowed.

Inductive prod: Type :=
| pair (n1: nat n2: bool).

I get a "The reference n2 was not found in the current environment" complaint.

When I make both arguments nats, or both arguments bools, like this

Inductive prod: Type := | pair (n1 n2: bool).

it doesn't complain.

Solution

  • In between one set of parentheses you can only have arguments of one type.

    Inductive prod : Type :=
| pair (x y : bool).

    But you cannot indeed have several types, the syntax for it is to use several sets of brackets:

    Inductive prod : Type :=
| pair (x : nat) (y : bool).