coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Required Arguments in a Section

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Required Arguments in a Section
Date: Thu, 28 Jan 2021 10:44:19 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay3-d.mail.gandi.net
Ironport-phdr: 9a23:wW4OGRzKqr92RSHXCy+O+j09IxM/srCxBDY+r6Qd2u4fIJqq85mqBkHD//Il1AaPAdyKragVwLuG++C4ACpcuMnH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjVu8UMn4dvLqk9xx/Kr3BVf+ha2X5kKUickhrh5Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTzFPDJ2yb4UPDOQPM+hXoIb/qFQSohWzHhWsCeD1xzNUmnP706833uI8Gg/GxgwgGNcOvWzVotrvKKASTfq6zK/QwjvCbvNW3Szy55bSchA9vPqBWr1wftDPxkkzDQzFiE+cqYPkPzORzesCrXKb7/Z7WOK0iG4mqxpxojuuxscpj4nGmJgVxkrC9Spn3IY4PNu1Q1N0btC4CpVfrT2aN5doTcM4RWFloCU3xqAGt5C1ciUH1IkryRDdZvKId4WF7BztWPufLzp8inxpZrOyihWy/0W81OHwSMu53VJWoydZjtTBuXMA2h7V58OaRPV9+UKh1iyO1wDV8uxEIEY0lbDaK5E72LIwmIATvELeFSH1gEX7lLGaelgm9+Sy6enrfq/qqoKfOoJ6kA3yL6Ajl8ynDeglPAUDUHKX9fm42bH54EH0QrFHgucrnqTbrZzXI9kQqLSjDA9PyIkj7g6yDze439QcmnkKNEhFdwyDj4fzO1DDLun0Auqlj1SpijhrxvTGMqfuAprXKHjMjbbhcax760FC1Ao/1dFf55RKBbEdOP//RFL9ud7CAhI7LwC42fvrBdZz248ERG6CBq+UPLvXsVCS5+IvJ+eMZJUSuDb4M/Ul6OThgmElmVAHe6mlx5QXaHG8Hvt9PUqZe2bsj8waEWcJvgs+V+/qiFyHUT5WeXmyRbgw5jclB4K6FYvDXJyigKSd3CenGZ1bfnxJCleVEXvxa4qEX+oMZzmJL896kj0EUKChRJU72RGvsg/60btnIfDO9i0Wr5KwnORysubUjFQ58SF+J8WbyWCECW9uzU0SQDpj86n8vUV7/XiC1aJ1meAQQdNa6u9AVEE1NJrWwvZmI8vxSxnCf9KMRUzgRNi6V2JiBuktysMDNh4uU+6piQrOinLzX+0l0oeTDZlxyZrymmDrLp8jmW3FxbIijlwjT9EJM2C61PYmplrjQrXRmkDcrJ6EMKEV3SrD7mCGlDTcp0JJSw1xVKDIRzYZa1eE9I2ktHOHdKenDPEcCiUEycOGLfEXOMfkiVxXH7LvftHXYmb3lG62CRfOwL6QPtLn

That won't work for eg `Definition foo := 0.`

Gaëtan Gilbert

On 28/01/2021 08:48, Pierre Courtieu wrote:

Hi, you can define a default "proof using" annotation in a section:
https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/proof-mode.html#proof-using-options

The default annotation is only added to a lemma only if there is not
already an annotation.

Proofgeneral has a mode to fill this annotations (see menu Coq/"Proof
using" mode.../), either by right clicking the "Proof" command
(default mode), or by making it fully automated (if there is no Proof
using then insert the one suggested by Coq.

Best regards,
Pierre

Le jeu. 28 janv. 2021 à 00:54, Kristina Sojakova
<sojakova.kristina AT gmail.com> a écrit :

Dear all,

Is there a mechanism for making an argument introduced e.g., via a
Variable in a Section required? That is, I want all definitions made in
that section to take this argument, not just the ones that use it.

Thanks,

Kristina

[Coq-Club] Required Arguments in a Section, Kristina Sojakova, 01/28/2021
- Re: [Coq-Club] Required Arguments in a Section, Pierre Courtieu, 01/28/2021
  - Re: [Coq-Club] Required Arguments in a Section, Gaëtan Gilbert, 01/28/2021
    - Re: [Coq-Club] Required Arguments in a Section, Pierre Courtieu, 01/28/2021