The Coq mailing list

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

Hi Miroslav,

I understand it now, thanks for your kind help, too. (∩_∩)

Best,

Zheng Yang

2017-04-13 16:40 GMT+08:00 Miroslav Dobsicek <m.dobsicek AT gmail.com>:

Hi Zheng,

you have probably heard that "if you happen to have f:False then anything follows".
In the same vein, f:False can be matched with anything.

Definition test_False_match (f:False) :=
  match f with
  | _ => true
  end.

Check test_False_match.

Best,
Miroslav

On 2017-04-13 09:01, zheng yang 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?