coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Differences between [let '(...)] and [let (...)]?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Differences between [let '(...)] and [let (...)]?
Date: Thu, 13 Oct 2016 18:58:19 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f46.google.com
Ironport-phdr: 9a23:3NRJ5BI5xUp0AapdzdmcpTZWNBhigK39O0sv0rFitYgXIv/xwZ3uMQTl6Ol3ixeRBMOAuqgC17ad6vu7ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaU0cjz2kJLh2MR+erAPLt8BQj5E0eYgrzR6cgHJTfOIe6nlvPknbyxT1/cC284Rk6D8Bk/0k/s9EF679evJrHvRjED06PjVtt4XQvh7ZQF7X6w==

What's the difference between [let '(a, b) := x in y] and [let (a, b) := x in y]? I had in my head that the first was better, but the first results in typechecking failures in 8.4 and anomalies in 8.6 (https://coq.inria.fr/bugs/show_bug.cgi?id=5140), so now I'm curious what the actual differences betwen them are.

Thanks,

Jason

[Coq-Club] Differences between [let '(...)] and [let (...)]?, Jason Gross, 10/13/2016
- Re: [Coq-Club] Differences between [let '(...)] and [let (...)]?, Hugo Herbelin, 10/17/2016
  - Re: [Coq-Club] Differences between [let '(...)] and [let (...)]?, Jacques-Henri Jourdan, 10/17/2016