The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.