The Coq mailing list

[zheng yang <zyang.uestc AT gmail.com>]

Hi Théo,

Yeah, I see, thanks for your help, too. O(∩_∩)O~

Best,

Zheng Yang

2017-04-13 16:12 GMT+08:00 Théo Zimmermann <theo.zimmi AT gmail.com>:

Hi Zheng Yang,

You should not get confused by your first line:

Parameter x : Set.

It has no impact on the pattern-matching where x is just a pattern which can bound anything to x.

Since you don't use x, it is equivalent to writing

Definition false_rect (n : nat) (f : False) : nat :=

  match f return nat with | _ => O end.

For the rest of the explanation, Anton Trunov has been faster than me ;-)

Best,

Théo

Le jeu. 13 avr. 2017 à 09:02, zheng yang <zyang.uestc AT gmail.com> a écrit :

Hi all, 

I am a fresh user of Coq, and I have a question. I find that the following definition typecheck in Coq:

Parameter x : Set.

Definition false_rect (n : nat) (f : False) : nat :=

  match f return nat with | x => O end.

And it is allowed in Coq. However, False does not has any constructor. Why does it work?