The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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