coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about fold and, probably, inductive definitions

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about fold and, probably, inductive definitions
Date: Mon, 1 Feb 2016 11:37:58 -0500
Authentication-results: mail3-smtp-sop.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:7Ub8pBdIJZb8ioPycmwZJzSZlGMj4u6mDksu8pMizoh2WeGdxc6+YR7h7PlgxGXEQZ/co6odzbGG7Oa5ACdavN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcSKKF8VzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB04SEx9FBRTy1BDmG9LatiLnuud5kH2ROcDzQLYoHyyj849kTRbpjGEMMDtvozKfsdB5kK8O+EHpnBd42YOBOIw=

On 02/01/2016 11:25 AM, Cedric Auger wrote:
> I even tend to be a little more "extreme" when I write fixpoints:
> when I write a fixpoint, I almost always try to have the indices of
> the inductive as arguments only (that is almost the minimal set of
> arguments which do not change between recursive calls).

I do not like this style much; it makes the function signature hard to read.

> With this way to write things, it is always obvious on which
> arguments recursion is performed, and minimizes the number of
> arguments to write in recursive calls.

Wouldn't a {struct} annotation do the same?

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Question about fold and, probably, inductive definitions, Ilmārs Cīrulis, 02/01/2016
- Re: [Coq-Club] Question about fold and, probably, inductive definitions, Robbert Krebbers, 02/01/2016
  - Re: [Coq-Club] Question about fold and, probably, inductive definitions, Ilmārs Cīrulis, 02/01/2016
    - Re: [Coq-Club] Question about fold and, probably, inductive definitions, Cedric Auger, 02/01/2016
      - Re: [Coq-Club] Question about fold and, probably, inductive definitions, Clément Pit--Claudel, 02/01/2016