The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hello,

> An idea could be to also provide the [A : Type] syntax in binders for
> non-maximal implicits, similar to what Arguments accepts.

That would indeed be a useful feature to have.  (A year ago or so, I had
asked on this list as I wondered whether such a feature is already
available.)
Is there a place where you track such feature requests (e.g., is this
worth opening an issue for in Bugzilla)?

Kind regards,
Ralf

> 
> Maxime.
> 
> On 09/15/2017 02:54 PM, Soegtrop, Michael wrote:
>> Dear Pierre,
>>
>>  
>>
>> I thought about using the curly brace notation for implicit arguments in
>> the standard library:
>>
>>  
>>
>> Inductive sig2 {A:Type} (P:A -> Prop) : Type :=
>>
>>     exist2 : forall x:A, P x -> sig2 P.
>>
>>  
>>
>> I think this is the most readable option for beginners and advanced
>> users. But it leads to a slightly different definition (see below),
>> first regarding the “maximally inserted” property – not sure why this is
>> different for “explicitly implicit” arguments and “Implicitly implicit”
>> arguments. There don’t seem to be any “Set/Unset Maximal Implicit
>> Insertion” directives in the code.
>>
>>  
>>
>> More interestingly the second argument of sig2 has a different scope
>> (type_scope for sig vs function_scope for sig2). No idea why this is so.
>>
>>  
>>
>> Such context dependent differences make it sometimes difficult to
>> understand definitions in the standard library.
>>
>>  
>>
>> Best regards,
>>
>>  
>>
>> Michael
>>
>>  
>>
>> Inductive sig (A : Type) (P : A -> Prop) : Type :=
>>
>>     exist : forall x : A, P x -> {x : A | P x}.
>>
>>  
>>
>> For sig: Argument A is implicit
>>
>> For exist: Argument A is implicit
>>
>> For sig: Argument scopes are [type_scope type_scope]
>>
>> For exist: Argument scopes are [type_scope function_scope _ _]
>>
>>  
>>
>> Inductive sig2 (A : Type) (P : A -> Prop) : Type :=
>>
>>     exist2 : forall x : A, P x -> sig2 P
>>
>>  
>>
>> For sig2: Argument A is implicit and maximally inserted
>>
>> For exist2: Argument A is implicit and maximally inserted
>>
>> For sig2: Argument scopes are [type_scope function_scope]
>>
>> For exist2: Argument scopes are [type_scope function_scope _ _]
>>
>>  
>>
>> Intel Deutschland GmbH
>> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
>> Tel: +49 89 99 8853-0, www.intel.de
>> Managing Directors: Christin Eisenschmid, Christian Lamprechter
>> Chairperson of the Supervisory Board: Nicole Lau
>> Registered Office: Munich
>> Commercial Register: Amtsgericht Muenchen HRB 186928
>>