coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yannick Forster <forster AT ps.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] `where' instead of `let-in'
- Date: Thu, 22 Feb 2018 14:03:35 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=forster AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=forster AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
- Ironport-phdr: 9a23:lLSiVx9RUvylhf9uRHKM819IXTAuvvDOBiVQ1KB30eIcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoQNFeUBO+BYr4jhqFsNsBCwBQ6sBPn0yj9UmHD2x7Ax3uMvEQHBxgwgBM4Ov2rOrNjuLKcSSvq5zLTOzTXCdv9Wwi3y55LSchAlu/6MW69/fdDMxkYxDg7IiEibp4LiPzOQzOsNsm6b4vJgVeK1im4rsRtxrSa0xss2i4nJgJoZykra+iVl2oY1IsG4R1B0YN64C5tcrSeaOJVqQs4kXmpmuz46x6UbtZO1cyUG0pAqyh/FZ/GFaYSE/BLuWP6SLDp7nn5oeb2yiwys/UWuyODwTNe43VlXoidDj9LCrGoC1wbJ5ciCUvZ9/lmu2TKI1w3L9uFEO0E0lbbcK54n2LIwjJsSvV7eHi/wmUX6lbSWeV8+9eiy7+ToeLPmqYKGO4BplA7yKqUumsqhDuQkKgUCQmaW9Oum2LDn/ED1WrdHguconqTZqJzaIN4Upq+9Aw9byIYj7BO/Ai+o0NQfh3kHN05Fdwydj4XyI1HOO+r0Deq5g1StiTtr3OrJMaf7ApXJNHfDlqrucaxg5EFC0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m24MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5s94HF2YBvUIQS/bxlFCYGWpdYGypQ68mzikgTp+gDMLYT4m3hLWH0GG3E8sFNSh9FlmQHCKwJM2/UPAWZXfKe54zonk/TbGkDrQZ+1SrvQ7+xaBgK7CMqDUD84/l1Z1u7uTJkRg0+Xp4ApbEij3ffyRPhmoNAgQO8uVnu0UnkgWbyu5lhf0dDtVa/fdAVAt8OZOOl7UnWeC3YRrIe5KycHjjQtiiBmtuHM4rwsMJZQBnCZO/iBGGxCOjGbsckbDNCJFmqq8=
The problem disappears when y is assigned an explicit level:
Notation "x 'where' y := z" := (let y := z in x) (at level 40, y at level 0).
Notation "x 'where' y : T := z" := (let y : T := z in x) (at level 40, y at level 0).
Compute 5 + x where x := 4.
Compute 5 + x where x : nat := 4.
I just picked level 0, you might have to adjust the concrete value. Also, I think the levels in both definitions have to be the same, otherwise the first one won't be available after the second one is defined.
Best
Yannick
On 22/02/18 09:38, Jasper Hugunin wrote:
You could use a notation like
```
Notation "( x 'where' y := z )" := (let y := z in x).
Notation "( x 'where' y ; T := z )" := (let y : T := z in x).
Compute ((x * y where x := 2) where y ; nat := 3).
```
You can play with precedence levels how you like, to replace the parentheses.
Notice I used ; instead of : for the typing annotation, getting (y : T := z) seems to be a bit more difficult.
Pattern lets, like `let '(x, y) := p` are also not supported...
- Jasper Hugunin
On Wed, Feb 21, 2018 at 10:01 PM, N. Raghavendra <nyraghu27132 AT gmail.com <mailto:nyraghu27132 AT gmail.com>> wrote:
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
<mailto: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
- Re: [Coq-Club] `where' instead of `let-in', Jasper Hugunin, 02/22/2018
Archive powered by MHonArc 2.6.18.