Конструктор Coq не может принимать два аргумента разных типов?

Question

Я только начинаю работать с Coq и не понимаю, почему это не разрешено.

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

Я получаю жалобу "Ссылка n2 не найдена в текущей среде".

Когда я делаю оба аргумента nats или оба аргумента bools, как это

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

, он не жалуется.

Answer 1

Между одним набором скобок вы можете иметь аргументы только одного типа.

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

Но вы не можете иметь несколько типов, синтаксис для этого заключается в использовании нескольких наборов скобок:

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