coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] `where' instead of `let-in'

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] `where' instead of `let-in'
Date: Thu, 22 Feb 2018 11:31:10 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg0-f51.google.com
Ironport-phdr: 9a23:3kgegRHEAT3st1b+zfIzzJ1GYnF86YWxBRYc798ds5kLTJ7zosuwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/KhMNwlqxVrhGuqBNj2IPUfJ2ZOeBicq/BZ94WWWxMVdtRWSxbBYO8apMCA+QZM+pCsoLzu0EBrRS+BQa2GuPg1DlIiWLs3aIg3egqDAbL3AogHtIUqnvUo9X1NLoMXe230aXFwyvPYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7LgFWXrIzqJTKV1uIVvmib9epgVPiji3Q5pAFquDSvx8EshpHTho0L1lDE7yJ5wJorKty3VE57esSoEJ1OuCGGMYZ9X8AsQ3lwtSs4xbAKo4O3cDYKxZg9xBPSZeaLfoiV7h77SeqcLi10iG9rdb+7nRq/8UytxvfhWsS7zFpHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzwXT5ftFIUAwjKbbM5EhzqIpmpodsUnPAzX6mErxjK+ReUUk/van5/77bbXho5+QL450igfgPaQygsGyA+s1PhITU2SF+emwzr7u8EPjTLhKk/E6iqzZv4rbJcQfqK65GQhV0oM75ha5Dzamys4XnXYHLFJYZh6KjZXlNl/QLP3jAve/hk6jkDZvx/zcIrLhBZDNImDZkLj9ZbZ991JcyA0rwN9D4JJUE6gNL+73Wk/sr9PVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMYQSoXP2L+Uvz//ol34w31EHLpOkxZ8GVHftVNIga3+QbnrlnNoHHX0D9EJqSv3wgVKCTGQMPi3od6057zA/TomhCNGQaJqqhenL+mHzJJRZZmlYB1aAC36iP9GCSu0FZyKPeJA4yWYsWr2oSotn3har4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfktrkl0y1PF2q990aUBSY5joshRWwJ/DqbyivRgAomrCA3Ed9aNDl2hR4f+WGxjfpcK29YLJn1FNZCigxTEhXf4BrYUk/mTC8Rx/P+FmXf2IMl5xjDN06xz11Q=

I am sometimes finding it inconvenient to write

Definition foo : bar := let ident : term1 := term2 in term3.

especially when term2 has a long expression. Is there a way of
writing such definitions as

Definition foo : bar := term3 where ident : term1 := term2.

I find the latter style easier to understand when term2 is long.

Thanks,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] `where' instead of `let-in', N. Raghavendra, 02/22/2018
- Re: [Coq-Club] `where' instead of `let-in', Jasper Hugunin, 02/22/2018
  - Re: [Coq-Club] `where' instead of `let-in', N. Raghavendra, 02/22/2018
  - Re: [Coq-Club] `where' instead of `let-in', Yannick Forster, 02/22/2018