Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Inline declaration of minimally inserted implicit arguments

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inline declaration of minimally inserted implicit arguments


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Inline declaration of minimally inserted implicit arguments
  • Date: Tue, 13 Dec 2016 11:09:56 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:Z9ffSBS4FOMryaMdflHrt6lxCNpsv+yvbD5Q0YIujvd0So/mwa67YhCN2/xhgRfzUJnB7Loc0qyN4vumBzBLuc3J8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43EK81xFPrv31HM7BU2GVnDVeLnlPn+dz2+4RspXcD88k9/tJNBP2pN58zSqZVWWwr

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
>



Archive powered by MHonArc 2.6.18.

Top of Page