The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have submitted a bug report which, if fixed, would let you do this by making [D1] an alias/notation.

-Jason

On Jun 1, 2014 4:54 PM, "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.