coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Required Arguments in a Section
Date: Thu, 28 Jan 2021 08:48:19 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f170.google.com
Ironport-phdr: 9a23:Hs/VLhSwmCQLrUyv5Sh5tBK05tpsv+yvbD5Q0YIujvd0So/mwa6zYRCN2/xhgRfzUJnB7Loc0qyK6vGmAz1LsMbJ8ChbNsAVCFld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6I8xgHXrnZMdOhbwWBlLk+Xkxrg+8u85pFu/zlStv4768JMTaD2dLkkQLJFCzgrL3o779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcRctaSTBPDZ2gYIsOF+oBPPhXr4/hp1sVsBCyARCgCP7zxjNUg3P727Ax3eY8HgHcxAEvENwOv3bUotv7N6kcTP67w7XHwzjYc/NWwC3w5JTUfhw9o/yBW697f8rLyUkoEgPIlk+eqY37MDOPzOQCrXWQ4vRnVeKykW4ntwBxrSayxswxjYTJnoMVxU7e9SVj3ok5P8G3SElmYd6+DJtQtj+VN5ZtT8MtRmFnoic6yrkctZGneygKzY0qyhjCYPOIb4aG+AjsVPqNIThmnnJlfqqyigiv/UWvxeDxS8i53VlEoydbjtTAqGwA2wDd58SaSfZz8USs1zaS2w7T9O1JIUA6mKrfJpMh3LM8iIQfvFjfEyLwhU74gqiWdkA+9eip7eTqerTmppmGN491kA7yKKoumta5DO8lMQYOR3CW9fqg2LDn50H0Q7VHgucrnqTYsZ3WP9kXq6ylDwJTz40t8QywDy2839QdhXQHLExKeBaAj4XxPlHBOvH4DfOmj1StlDdn2unKPrP8DpjPMnTPirjhfbF6605TzAo808pT6I5TCrEEOP7zW0nxu8LEDhIhLQC43+LqBM9+244eQ26DH66UPaLIvVOV5O8jP/GAZIoPtzb8L/gl6eTujXg8mVIFZamp3IUYaGqiHvt4OUmWfX3sgsobEWcWvwoxUvHqhUaNUT5WfXmyXqY86isnB4KhCIfPXpqtj6CZ3CenAp1WYXhLBUyLEXfxbomLR/MMaD+JLcJ6iTwFVb2hS5c72h20tQ/6zaBnLuvO9SECu5Ljzos92+qGvhYrvRdwEs7Vh2qKViR/mn4Cbz4wxqF250JnnASty6991sRZGMZJ6rtiVRogKZ/R0qQuE9H/QBjMONyOVUy6Q9i7KT40R9M1hdQJZhAuSJ2Zkhnf0n/yUPcunLuRCclxq/qEhiWjF4NG03/DkZIZoRwmT89IbzP0g6d+803SA9eMnRzGz+ClcqMT2COL/2CGnzLX4BNoFTVoWKCAZkgxI1PMpI2gtEzHRr6qT78gN1kZkJ/QGu5xctTsyG5+arLmMdXabXi2nj7pVxmNz7KIKoHtfjdE0Q==

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