coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Bug w.r.t. Let Fixpoint & Section visibility

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Bug w.r.t. Let Fixpoint & Section visibility
Date: Thu, 15 Feb 2018 14:30:38 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 7.mo69.mail-out.ovh.net
Ironport-phdr: 9a23:aCXCYxBicpmWy74EgI4OUyQJP3N1i/DPJgcQr6AfoPdwSPvzpMbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs7Xiiv4qlpRRLmkSsLKzE0+3zThsFwkK5XpRSsrAF9zYHJeoGYLOdwcL3Tfd0aRmRPUMheWCNDDYygYIUCFPYBMORCooXhu1cDoxmzCA+xD+3v0D9IgXr20LU93es7HgDG3QkgEMwTu3rattL1Mr4VUfuox6TPyDXMdfJW2TPm5YjNaB8grvCMXbdufsXM10YvER3Kjk6KpYzrJTOYz+IAuHWV4epnUOKgkW8nqwdprzigx8cslonJhp8OxVze6Sp5x4M1KNulQ0B4ed6pCJRduiCAO4drXs8vQ3tktSYmxrEct5O3YjAGxZA6yxLFdvCKcpSE7gj+WOuVIDp0nm9pdbO+ihu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL6MWLUP59/kCg1DuLzQzT7/tLIUEwlabCLJ4h36IwmoAUsUTdHi/6gkP2g7GKdkk8++io7froYqn+q5KTNoJ4kBzyPrgul8ClAek0LhICUmaF9eik0b3s50z5QLFEjv0slanZtYjXJcEBqa64Bw9YyYMj5AywDjen1dQXg2QII0xDeB2ZlIjlIV/OIOrgAfeln1usiCtrx+zBPrD5HprNKWHDnK79crZ59k5T0xE+zctf5pJRErEOOuj/Wk73tNzCDx82KRa4w+j9CIY16oRLUmWWR6SdLan6sFmS5+tpLfPfSpUSvWPYIugk4vOmof4/GURVKayg3J8/bXmoH/FrL0ifbGGqjM1XQjRChRY3UOG/0A7KajVUfXvnAvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPz4UD1mcEHLle4iCVuxKZjjAe5Y9wAxBbqCoTsoa7T/rrBXzkuQ1K+PE+ygVuZ/l2cMz6feBzUhvpwwxNNyU1iS2d08xnm4MQGVrjv85pEsjmxGG2Kl8xvtFCZpU+fMPVAomZ8bR

Hello,

Would you mind reporting at https://github.com/coq/coq/issues ?

Thanks!

Maxime.

On 02/15/2018 02:17 PM, Dominique Larchey-Wendling wrote:
> Hi all,
>
> Maybe this is a feature but the following example shows a
> Let Fixpoint construct leaking out of a Section. Is this the
> desired behaviour (tested under 8.6 and 8.7.1) ?
>
> (****************************)
>
> Section visibility.
>
> Let Fixpoint ev n := match n with 0 => true | S n => od n end
> with od n := match n with 0 => false | S n => ev n end.
>
> Let Fixpoint ev' (n : nat) : bool
> with od' (n : nat) : bool.
> Proof.
> exact (match n with 0 => true | S n => od' n end).
> exact (match n with 0 => false | S n => ev' n end).
> Defined.
>
> Let my_even := ev.
>
> End visibility.
>
> Check ev'. (* succeeds (unexpected) *)
> Check my_even. (* succeeds as expected *)
> Check ev. (* fail as expected *)
>
>
> (****************************)
>
> I do not see why ev & ev' are treated differently?
>
> Thx in advance,
>
> Dominique
>

[Coq-Club] Bug w.r.t. Let Fixpoint & Section visibility, Dominique Larchey-Wendling, 02/15/2018
- Re: [Coq-Club] Bug w.r.t. Let Fixpoint & Section visibility, Maxime Dénès, 02/15/2018
  - Re: [Coq-Club] Bug w.r.t. Let Fixpoint & Section visibility, Dominique Larchey-Wendling, 02/15/2018