coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Beta Ziliani <beta AT mpi-sws.org>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Axioms reported by coqchk
- Date: Fri, 19 Aug 2016 09:42:27 -0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
- Ironport-phdr: 9a23:fpe3lRTIqePlhnN+HsGQERDqTdpsv+yvbD5Q0YIujvd0So/mwa64bBeN2/xhgRfzUJnB7Loc0qyN4vmmAzJLu8bJ8ChbNscdD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbshsi6n9q/54fUK10RwmHsOPUocl7s/U2R7pBQ2to6bP5pi1PgmThhQ6xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/TGKdwaE52MdX2MKiVIIRlGdtFCpFqv25wD9r6JW3DSQdZn9SqlxUjC/5Y9qTgXpgWEJLWhq3nvQj5lagb5S6CCgox12xY+cNIuYKPNWe7vcOMgFXixGRMkHBH8JOZ+1c4ZaV7lJBu1ftYSo4gJW9RY=
On Fri, Aug 19, 2016 at 9:16 AM, Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org> wrote:
On 08/19/2016 02:01 PM, Ralf Jung wrote:
I found the old thread:
<https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00168.html>
That explains what I am seeing as being the expected behavior. People
have been asking for suggestions back then, so here they are ;)
My proposal here would be to only show axioms which are actually used by
a name exported by one of the modules passed to coqchk.
Names which are not exported are still available via qualified names when importing the module, so this makes sense to include them in the list (i.e., if you are allowed to import the module, then you get the power to use these axioms).
Alternatively,
Program could provide means of importing the base functionality without
needlessly importing modules. What do you think?
But then how different is this from refine ?
Program
uses a bidirectional type-inference mechanism. This is the main use of Program
for me: a cleaner and bidirectional refine
(cleaner in the sense that visually Program Definition foo : type := term.
is nicer than Definition foo : type. refine (term).
).
Kind regards,
Ralf
- [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Matthieu Sozeau, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre-Marie Pédrot, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
Archive powered by MHonArc 2.6.18.