The Coq mailing list

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

Hi Anton,

Thanks for your kind help, I'm clear now O(∩_∩)O

Best,

Zheng Yang

2017-04-13 16:09 GMT+08:00 Anton Trunov <anton.a.trunov AT gmail.com>:

Hi Zheng Yang,

See chapter 17 of the reference manual. Here is the relevant quote:
The pattern-matching compilation strategy examines patterns from left to right.
A match _expression_ is generated only when there is at least one constructor in the column of patterns.
E.g. the following example does not build a match _expression_.
Coq < Check (fun x:nat => match x return nat with
                          | y => y end).

If you print back your `false_rect` definition, you’ll see the following
false_rect = fun (_ : nat) (_ : False) => 0
     : nat -> False -> nat

—
best regards,
Anton

> On 13 Apr 2017, at 10:01, zheng yang <zyang.uestc AT gmail.com> wrote:
>
> 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?