The Coq mailing list

[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?