coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jasper Hugunin <jasperh AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] `where' instead of `let-in'
Date: Thu, 22 Feb 2018 00:38:40 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasperh AT cs.washington.edu; spf=None smtp.mailfrom=jasperh AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ot0-f179.google.com
Ironport-phdr: 9a23:lAov7xLPSOiedXyyNtmcpTZWNBhigK39O0sv0rFitYgRI/7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhyUJNzA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoeyYJEUD+oZI+lYtZT2qVkTrRuxGAmsAuLvyjlVjXLx3601yf8hERnY0ww6H9IDq2jbrM7vOKYcS++116nIzTTFb/NZxTf9747Ifgo/rv6RQLJ9aMzcwlQhGQPCi1Wfs43lPzWN2+QNqWib7vBsVfixhG48sQ1xoz6vyt82iobXmoIV0FfE9Tlnz4c6Od24U1R3Ydi6H5tMsSyRKoh4Qts6Tmxqtys20KAKtYC7cSQQy5kr2QTTZ+GFfoWM5B/oSfyfLi1ihH1/fbKynxay/lakyu37TsS01UxFritBktXVsXANywDf5tGJSvdg/Eqs3SyD1w/U6uFDLkA0kbTUJ4Q9zb43k5ofqUXDHinol0XqlKKbdEop9vK15+j5YrjqvJyRO5Fuhg3jMKkjntSzAeEiPQgPW2ib9/681Lrm/UDhQrVFlOY2krHHv5DAJcQWvbK2AxRP3oct8Rm/FDem0NUenXkIMFJFfxSHg5L3NF7TPfD0Fe2/jEi0kDd32/DGOaXsDYnKLnjaibvuYbJ961NHxwco1tBe55dUCqkbL/7pW0/xssbYDh4jPACuzebnEoY16oRLUmWWR6SdLan6sFmS5+tpLfPfSpUSvWPfIuM96uSmrWI2hFkce+H935IMcH2iHtxtOAOGaGHsg9EODWAM+AcyUbq52xW5TTdPaiPqDOoH7TYhBdf+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFC65JY6fHegFcyKTJMB9lTpCWLS8Gdd4iUOe8TTiwr8iFdL6vzUCvMuyhtNuofLajhEz8zNoCMLb3m2QHTktwzE4AgQu1aU6mnRTj1eO1a8i3a5dHN1XovRVCkI0bMGNieN9DN/2V0TKedLbEFs=

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> 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>, 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