coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] `where' instead of `let-in'
Date: Thu, 22 Feb 2018 14:49:02 +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-f44.google.com
Ironport-phdr: 9a23:d1NYBBXIbJ2YxIObV0MDGnkvxZTV8LGtZVwlr6E/grcLSJyIuqrYbBKGt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kaBUoByvqBxlzYDaY46aO+Zlc6PBYd8XX3ZNUtpLWiBdBI63cosBD/AGPeZdt4TxqUMAoQGjDgewHuzvxT9IiWXo3aIk1eQuDBvG0xYuE9kTt3nUqtX0NL0IXuC6zKnI0CvPYvFL1Trz9oTFaR8hofSWUrJxdcrd01UgFwTAjliJr4HuIj2b1uMIs2eB7upgU/qii249qwFwuDSv3NkjipLTioIUzFDI7T95z5gpJd2iT057fcCrEZRMtyGBLYd2RN0tQ31utS0nybMGoYa2cSoFxZg92hLTdfyKf5KL7x/tTuqcLjh1iGp4dL+wnRq+7Eatx+nmWsS01FtGtDdJn9bQun0Lyhfd8NKISuFn8UekwTuP1x7c6uVDIU0skKrUMZ8hwropmpoLvkTPAjb6mEv5gaKZbEkk9e+o6+PoYrXiuJCQLZN7igb7Mqg2m8y/B/o3MhQWUmWZ9umwzqDv8VP5TblQjfA7nLPVvZ/VKMgDo662GQ5V0oIt6xalCDem1cwVnX8HLVJfYh2HgIjpO0zQLP36EPuyjUqgnSxkx/DDJLLhA5HNImLfn7fmeLZx81RcxxYrzdBD+5JUDakML+70Wk/ordDXEhs5MxGvzOv8E9V81oYeWXqVDaODMaPSt0WI5uM1LOWWao8VomW1F/9w7Pn3yHQ9hFU1fK+z3JJRZmrrJPl+J1SlZi+mpJFJK24FvgMgQermklTIGWpVdmy7UKIhvG5iU9iOAoLKR4Tri7uEinSVBJpTMypgTBi2GHjofpuJXfsWYWjadslwiDULVaX7FNZ6jzmhsQb7z/xsKe+CqX5Qjo7qyNUgv76brho17zEhV53MgVHIdHl9myYzfxFz2al+pUJnzVLaiPp3hvVZEZpY4PYbC15mZ66Z9PRzDpXJYiyEZs2AEQ/0TdCvADV3RdU0kYdXPhRNXu66hxWG5BKERr8Yk7vRWc4x+6PYmmD+f4NzlyqA264mgF0rBMBIMD/+iw==

At 2018-02-22T00:38:40-08:00, Jasper Hugunin wrote:

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

Thanks for the suggestion.

I find it confusing to use `;' instead of `:' to indicate the type of a
term. In the absence of any other solution, I guess I will just rewrite
and split the definition so that term3 becomes short.

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