coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] When does the termination checker reduce a record accessor?

From: "William J. Bowman" <wjb AT williamjbowman.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] When does the termination checker reduce a record accessor?
Date: Fri, 3 Nov 2017 16:00:02 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=Pass smtp.mailfrom=wjb AT williamjbowman.com; spf=None smtp.helo=postmaster AT mail.williamjbowman.com
Ironport-phdr: 9a23:jEh0Rh0foj1EHw3hsmDT+DRfVm0co7zxezQtwd8ZsesQL/ad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tLw6annrn5jkLXx77KABdJ+LvG4eUgd7k+fq1/siZXARMgDu0ZPtQal2cqhrUv89cyd99KKwZ1RrNpnpBfuZcwnxtLFTVlBH5sJTjtKV/+jhd7qpyv/VLVr/3Kvw1

> On Nov 3, 2017, at 3:39 PM, Joachim Breitner
> <mail AT joachim-breitner.de>
> wrote:
>
> Without δ, why does it unfold `list_P` and `existsb` to see that the
> recursion on the list is nicely structural? And why do tree_P1 and
> tree_P2 still work even when I specify Opaque list_P.?
I was about to conjecture exactly what you discovered; thank you for digging
into the source. And the question you pose is most mysterious. Are some
definitions treated differently than others?

—
William J. Bowman

[Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
- Re: [Coq-Club] When does the termination checker reduce a record accessor?, Tej Chajed, 11/03/2017
  - Re: [Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
- Re: [Coq-Club] When does the termination checker reduce a record accessor?, William J. Bowman, 11/03/2017
  - Re: [Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
  - Re: [Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
    - Re: [Coq-Club] When does the termination checker reduce a record accessor?, William J. Bowman, 11/03/2017
      - Re: [Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
        
        Re: [Coq-Club] When does the termination checker reduce a record accessor?, Joachim Breitner, 11/03/2017
    - Re: [Coq-Club] When does the termination checker reduce a record accessor?, Maxime Dénès, 11/03/2017