Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about Pattern Matching on False

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Pattern Matching on False


Chronological Thread 
  • From: zheng yang <zyang.uestc AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Question about Pattern Matching on False
  • Date: Fri, 14 Apr 2017 10:29:52 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=zyang.uestc AT gmail.com; spf=Pass smtp.mailfrom=zyang.uestc AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f169.google.com
  • Ironport-phdr: 9a23:zho8jR8L0kxp3f9uRHKM819IXTAuvvDOBiVQ1KB52uwcTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRx3miCkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTy1AAoOiYIsJAOoKIOZZoJP7p1sBsBCzAgitBeP1xT9OiX/6x7A63Po6EQHawAMtBN0OsHHOo9X0MKceS/y6zK7NzTjaaf5dxDTz6JDQfxw/vf2BWah8fMnRxEU1CQ/JkFudpZb4Mz6U0ukAtXWQ4fB6WuK1kWEnrhl8ojixyccojYnEnocVxUrF9SV92Yo1JNq4RFJibd6qDZddtiWXO5F5QsMlRGFotyI6xaMctZGneygKzYwrxx/Za/OZb4iF+gzvWPqVLDtih39oeKiziwis/UWu0OHwS8i53VJSoipAiNbMt3QN1xLJ6siAT/tw5kag2DaV2ADV5eFIO100mrTAK5493rE9jZUTsUHZES/3nEX6lrOZdkIh+uSw8eTofq3mpoOAN49zkgzxLqMumtWmDeskNggOQnOU9P+n1Lzj+E35WK9Fguc3kqnfqpDaJN4UqrS3Aw9Pgc4f7EO0CC7j29AFl1EGKkhEcVSJldvHIVbLdeL4APGwy0Wlljgjk+LXN7vuRIjANWTIuLjkdLd5rUVbzVxgnphk+5tIB+RZc7rIUUjruYmAAw==

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?




Archive powered by MHonArc 2.6.18.

Top of Page