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: [Coq-Club] Question about Pattern Matching on False
Date: Thu, 13 Apr 2017 15:01:43 +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-f177.google.com
Ironport-phdr: 9a23:9gpEHBFVIXtnrON+OsKOPJ1GYnF86YWxBRYc798ds5kLTJ79rs6wAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZA4K8b5UAD+wOPe1Fr4jyvV0OrRSjDgSrBeLuyiVHhnn53aEgzuQuDxrG3BA8EN8Vv3TUqc/6NKYWUeyv0KbIyjDDYupQ1Dzg64bIaggsre+QUb90a8bcykkiGxnbglmOp4HpJS6Z2+YPvmWd8uFuT/igi3Q9pAF0ujWvxtkjio3Oho8Nz1DL7yR5wIIsKd25T053fceoEJVNuyyYNYZ6WMwiQ2ZvuCY1zr0Jp4S3czQNyJQi3xLfavqHfJaU4h/7SuqdPTN1iGhmdb+/nRq+71asx+PmWsWp0ltHrDJJktzWuXAM0xzT5NKHSvx4/kq52DeO1xrc6udLIUwuiKrUNYUhwqIsmZcIvkTDGzX5mETyjKOMakok/e2o5/z9Yrr6vp+cK5N0igbmP6syncy/GP00PRQKX2iG4uuxz6bj/E38QLVSlPI6iKjZsJbAJcQavKG1GQFV0pxwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtH/eyhVvkgT5tyLiSLKzoBJqLM3XYjLzJcrN06koaww02m4MMr6lIA60MdaqgEnT6s8bVW0c0

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