The Coq mailing list

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

Yes, but I guess this is not what Ralf is asking for. He's asking if
there is a way to manually annotate some arguments to make them implicit
but not maximally implicit. "Set Implicit Arguments" makes Coq infer
such annotations, not always in the desired way.

To my knowledge, there is no way of doing it, apart from using
Arguments, as Ralf mentions. I don't know why we have the {A : Type}
syntax but not [A : Type] in binders, whereas Arguments has both. Maybe
historical reasons (v7 binders syntax).

There might exist an option that I'm not aware of, though. If not, a
pull request extending the binder syntax would be welcome :) Or even a
CEP, to see if people expect any problem with such an extension.

Maxime.


On 12/13/16 11:05, Théo Zimmermann wrote:
> I may very well have misunderstood your question but isn't Set Implicit
> Arguments what you are looking for?
> 
> Set Implicit Arguments.
> 
> Definition foo_id (A : Type) (a : A) := a.
> 
> Print foo_id.
> (*
> foo_id =
> fun (A : Type) (a : A) => a
>      : forall A : Type, A -> A
> 
> Argument A is implicit
> Argument scopes are [type_scope _]
> *)
> 
> A is implicit but not maximally inserted.
> 
> Théo
> 
> Le mar. 13 déc. 2016 à 10:58, Ralf Jung 
> <jung AT mpi-sws.org
> <mailto:jung AT mpi-sws.org>>
>  a écrit :
> 
>     Hi all,
> 
>     is there a syntax to make an argument of a Definition *minimally*
>     inserted?  I know the following syntax:
> 
>       Definition foo_id {A : Type} (a : A) := a.
> 
>     However, this makes A *maximally* inserted.  Of course I can then use
>     Arguments to make it minimally inserted, but (a) this has the potential
>     of de-syncing with the definition and (b) the place where I need this is
>     a section variable where I would have to re-declare Arguments for each
>     definition inside the section. That's not a scalable option.
> 
>     What I am looking for is either an option ("Set ...") to configure
>     whether the curly braces make arguments minimally or maximally implicit,
>     or another syntax (an alternative to the curly braces) that makes them
>     minimally implicit.  Does something like that exist?
> 
>     I found "Unset Maximal Implicit Insertion.", but that affects only the
>     arguments that are automatically made implicit, not those that are
>     declared implicit by using curly braces.
> 
>     Kind regards,
>     Ralf
>