The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Michael,

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

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
>