coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Semantics of lazymatch in 8.5

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Semantics of lazymatch in 8.5
Date: Wed, 12 Oct 2016 17:03:53 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:taYB4BLFh4cZLxk66NmcpTZWNBhigK39O0sv0rFitYgUK/jxwZ3uMQTl6Ol3ixeRBMOAuqgC17Cd6v28ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9Msfogs+2z+G//YHIK0UN3WLlIOA6EBLjhgLI/uISnIEqfq02017CpmZCU+VQ32JhY1yJyUXS/MC1qbVnciFdve4Wz89cFODRe60lQbFcRGAtN20w6cv38wHCUSOA43IdViMdlR8eUFuN1w3zQpqk6niyjeF6wiTPeJSuFb0=

Hi coq-club,

The CHANGES file says:

- Matching using "lazymatch" was fundamentally modified. It now behaves
like "match" (immediate execution of the matching branch) but without
the backtracking mechanism in case of failure.

The description of the new behaviour sounds close to what my understanding of
lazymatch was in 8.4 (as long as the result of the lazy match isn't bound to
a variable). Beyond the 8.4 issue that caused lazymatch to backtrack when a
branch contained a type error, what are examples of differences between the
old and the new lazymatch?

Thanks!
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Semantics of lazymatch in 8.5, Clément Pit--Claudel, 10/12/2016
- Re: [Coq-Club] Semantics of lazymatch in 8.5, Jonathan Leivent, 10/12/2016
  - Re: [Coq-Club] Semantics of lazymatch in 8.5, Jason Gross, 10/13/2016