coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Required Arguments in a Section

From: Kristina Sojakova <sojakova.kristina AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Required Arguments in a Section
Date: Thu, 28 Jan 2021 00:53:51 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sojakova.kristina AT gmail.com; spf=Pass smtp.mailfrom=sojakova.kristina AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f44.google.com
Ironport-phdr: 9a23:MuB2xBTivW0VM3iq/2h7QSQzLNpsv+yvbD5Q0YIujvd0So/mwa6zYRaN2/xhgRfzUJnB7Loc0qyK6vGmAz1LucbJ8ChbNsAVCFld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6I8xgHXrnZMdOha2WBlLk+Xkxrg+8u85pFu/zlStv4768JMTaD2dLkkQLJFCzgrL3o779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWMtaSi5PDZ6mb4YXEeQPPftWoYrzqVQAohSxGQaiCfjzyjJKnHL6wbE23uojHAzAwQcuH8gOsHPRrNjtMakSS+G1zLLUzTXCafNZwyr25pXPchAju/6MXrVwcdTLxkIyEA7FlVKQqY7/MDOW0eQNrXKU4/BjVeK1im4nsB1xojmpxsg2kYTJiYcVxUrF9SV92oo6Odq4SEtibNOiDZBfuD2UOZFsTcM+X2Fnpjw6yrsetJKmfCYHyIoqywPeZvKHbYWE/xPuWumfLzp7gH9oeb2yihSu/EWjzuDyWNW43VRFoCRFjNTAqGwA2wHN5sWJV/Zw+Fqq1zWX1w3L9O1IPUQ5mbDYJpMh2LI8i4QfvEfZEiL5l0j6lLGaelk49uS17unqYbTrqoKZOoJ6lg7xLqojl8mxDOk7LAcCQ22W9vig2LDi+ED2WrVHg/I5n6TctJ3VO8UWqrC8DgBIyIku7wiwAjG729oCh3YHNkhKeBefgojpJV7OJPf4AO+6g1u2kTdrw+nKP7PkApnQN3TDnrjscLln505Tzwozyt9f55ZKBb0bPP3zXUrxuMTZDh8/LQO03/7qBMth2o4aQ26CAa+UPLnPvVOW5e8jOeaBaYANtDb4Mfcl5vrujXEjmV8aeKmkxYAXaHe6Hvt8IEWZZmTsjc0bHWcJpAo+TffqiEGDUT5VfXm/RK085jQhB4KnCYfPXJyigLuE3CujBJ1ZenhGCkyQEXfvb4iLR/AMaDuLLsB9ljwESKOuRpQ61RCusQ/606BoIvDV+i0er5Lj1cJ66/fdlREopnRICJGW1HjIRGVplEsJQSU31eZxux9T0FCGhItigudEFNpar8hOUA45MoDVh7hhDNL7WQXfd5GKUle9XtSgCBk+S9swx5kFZEMrSIbqtQzKwyf/W+xdrLeMHpFhqvuBjUi0HN50zjP97Idkj1QiRZESZ2ivh6o66A2KQoCVzwOWkKGlcala1ynIpj/akTi++XpAWQs1ap3rGGgFbxKP/9v870LGCbSpDOZ/a1oT+Yu5MqJPL+bRoxBDTfbnNs7ZZjvoyWi1DBeMgLiLadizdg==

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