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 13:10:30 +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-f181.google.com
Ironport-phdr: 9a23:zJGO1xXREYuxUe+v+M8odtKPg7TV8LGtZVwlr6E/grcLSJyIuqrYbRaHt8tkgFKBZ4jH8fUM07OQ7/mxHzdYqszR+DBaKdoQDkBD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs1xxfTrHZEZ+tayX1rKFmOmxrw+tq88IRs/ihNuf8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ91cXDJdDIyic4QPDvIBPedGoIn7u1sOtga1CQ21CO/y1jNEmnr60Ksn2OojDA7GxhQtEN0AsHvWrNv7OqQcX/2rwqbUwjvOdO9W2S7n5YTUbhwtvfOBULRtesTR00kvEAbFg02Kp4zkITyVzP4NvHaG5Od+UuKvlnQnqx1wojex28cnl47EhpoUyl/a7yV52pg6KcekR058fN6kCodQtyCEOItrWc4iTGRotzw7yr0Co5K0YC8KyJE+yhPZdveIfJSG7Aj5W+aNPTd3mmhleLSnihus70Suyu3xW9So3FtWoSRIksTBu2wM2hHN5MWKRfRz80W91TuO0w3d5P9ILV02mKTVNpMvzb4+mocOvEnAESL7nlj9gqyOdkg85OSk9+Dqbq/lq5KcLYN4lwDzP6U0lsCiAuk0Lw4DVHWB9+umzr3s50j5Ta1KjvIolqnZt4jXJcEBqa64Bw9Zy4cj6xKiAzu/3tQUgHoKIE9fdBKIiIjpPF7OIPTmAvuln1uslzJry+jHPr3nHJrNMmDOnKn9cbt58UJRywo+wcpC659VC7wNOu//V0zsuNDACx82KQ20w+LpCNVn0YMeXHqCAreYMKzMq1+I/PwgL/OQa48SpTb9MeQl5//wgn8kglIdcqyp0oEWaHC8BPhpP0KZYX/0jtcbDWgKphY+TPDtiFCaTTFTYG+yU7sg6TE/FYKpFpzORputgbyExCe0BIdaZmFAClCWEHfnbZ+IW/kWaHHaHsg0uTsdHZOlVoVpgRqprUrxz6dtBuvS4CwR85z5gotb/erWwCkz+CZuAoy21HyXU2B5gytcXz47xrpy50d6102f0KVlq/NdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTRQPjG43+WG1jfpcK29YLJn1FNZC6lBmahnilBrYUk/qAA5lmqvuNjUi0HN50zjP97IdkilAnRsVVMmj/3/xw8gHSA8jClEDLzv/3J5RZ5zbE8SK49UTLvExcV1QuA6DMXHRaZ0+P6NqgthqEQLipBrAqdABGzJzaJw==

Le jeu. 28 janv. 2021 à 10:44, Gaëtan Gilbert
<gaetan.gilbert AT skyskimmer.net> a écrit :
>
> That won't work for eg `Definition foo := 0.`

Indeed. It only works for interactive proofs starting with Proof.

Set Default Proof Using "X".
Definition foo: nat.
Proof. (* mandatory *)
exact 0.
Qed.

Remark: in v8.13 one can set the "using" attribute explicitely on definitions

#[using="X"] Definition foo:=0.

but it does not seem possible to set a default value to it. Maybe this
deserves a feature wish?

Best,
Pierre

[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