2

I am reading Software Foundations(*) and have an issue with defining types in Coq: In the example below I tried to make 2 type definitions. t1 is the list of naturals, and t2 is a pair of naturals.

The first definition t1 is accepted by Coq but definition t2 is rejected with the error message:

The term (nat, nat) has type (Set * Set)%type while it is expected to have type Type.

I don't quite understand what is wrong and what this message means. What is wrong with definition t2?

  Definition t1 : Type := list nat.
  Definition t2 : Type := pair nat nat.

(*) http://www.cis.upenn.edu/~bcpierce/sf/Lists.html#lab58

Improve this question

1 Answer 1

Reset to default
5

No, pair is the constructor, prod is the type.

Print prod.
Check prod.
Check @pair.

Definition t1 : Type := list nat.
Definition t2 : Type := prod nat nat.
Definition t2' : Type := (nat * nat)%type.
Improve this answer
2
  • Pair is a data constructor and prod a type constructor?
    – Maarten Faddegon
    Commented Apr 25, 2014 at 8:28
  • 2
    Right. pair x1 x2: prod t1 t2, or using their notations, (x1, x2): t1 * t2.
    – user3551663
    Commented Apr 25, 2014 at 14:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.