The Coq mailing list

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

Hi,

> I may very well have misunderstood your question but isn't Set Implicit
> Arguments what you are looking for?

This will automatically determine which arguments are implicit and which
are not.  We prefer to define this explicitly to avoid surprises about
which arguments are and which are not implicit.

Kind regards,
Ralf

> 
> 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
>