coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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>:
Since you don't use x, it is equivalent to writingIt has no impact on the pattern-matching where x is just a pattern which can bound anything to x.Hi Zheng Yang,Parameter x : Set.
You should not get confused by your first line: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éoLe 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?
- [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/13/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Anton Trunov, 04/13/2017
- Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Théo Zimmermann, 04/13/2017
- Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Miroslav Dobsicek, 04/13/2017
- Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Anton Trunov, 04/13/2017
Archive powered by MHonArc 2.6.18.