The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

As I remember, Agda used to have such type definitions including implicit parameters. It proved quite complicated to handle. I remember an Agda meeting where the issue was raised. I don't know what the status is now, though.

When Matthieu Sozeau decided to import this feature into Coq, we were aware that it would be most complicated to port the type declaration part (plus we had to count on Coq's legacy too). So there was no attempt to do so. I agree, however, that it would be most convenient to have something along these lines. It's unclear to me what precise form it should take.


/Arnaud Spiwack

On 1 June 2014 17:53, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

Not that I am aware of, if you do

  Definition D1 : Type := forall {T : Type} (x : T), Type.

Coq tells "Warning: Ignoring implicit status of product binder T and following binders". You could create a feature request.

An alternative is to create an auxiliary definition or notation, like

  Definition foo (A : D1) {T} (x : T) := A T x.

or

  Notation foo A x := (A _ x).

And then write

  Definition DD1 (A : D1) := forall x : bool, foo A x.

Depending on the use case, this may actually be worse...

On 06/01/2014 03:12 PM, Vladimir Voevodsky wrote:

Hi,

I have a type of the form (I am using a simplified example):

Definition D1 : Type := forall ( T : Type ) ( x : T ) , Type .

I now have other definitions which use D1 as a type of a parameter:

Definition DD1 ( A : D1 ) := ....

Definition DD2 ( A : D1 ) := ....

etc.

I am going to use A : D1, mostly, fully applied i.e. in the form  A T x . I do not want to write T in A T x all the time since it can be easily inferred from x . Is there a way to write something like:

Definition D1 : Type := forall { T : Type } ( x : T ) , Type .

and then to write A x ?

Vladimir.