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: Anton Trunov <anton.a.trunov AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Question about Pattern Matching on False
  • Date: Thu, 13 Apr 2017 11:09:35 +0300
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f45.google.com
  • Ironport-phdr: 9a23:A40kshSOX0QJXWZ2YVxeWWabiNpsv+yvbD5Q0YIujvd0So/mwa69YBON2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHLhcJ/g61VvRyvpxJhzYHWY4+bM+Fzfr/EfdMfWWZBXtpdWi5HD4ihb4UPFe0BPeNAooThoVsOsRy+BQ+xD+3x0D9Im3n23aok0+88FgzJxgogH84JsHTSttn6Lr0eUfyvzKnVyzXDaO1W1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUiTp4z9Jz6ZyPgBvmyB4+djVe+jkXArpxxxrzS1ycohipHFip8Rx13E7yl13YI4KcCiREJmbtOpEYFcuzybOoZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbvyIaYmI4hb6WOaVLzd0mGtpeLywihuy60Sgxer8Vs670FZOsCVJiMXDtncI1xDL68iHTOVy/lu51DqRywze7vtILEM0mKbBNZIt3749moAcvEnDBiP2nV/5jK6SdkUq4Oio7OHnb638qZ+aK490jQf+Pr40lcClHeQ4KBUOX26c+eSiz7Dj8kj5T69Ljv0yiKXWrJfaJcEDqq6jHwBVypoj6wq4Dzq+zNsYmmAHIEtZdxKDkojmIErDIOv4DPe6m1Sjii1nx/HAPr37A5XCNGLPkLn7feU110kJww0qiNtb+ph8C7cbIfu1VFWimsbfC0oQNRCzxa7bEsh70Z1WDWuJHqifdqqUrUWV4OUxC+aJbY4R/j36Lq52tLbVkXYllApFLuGS1pwNZSXgEw==

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?




Archive powered by MHonArc 2.6.18.

Top of Page