The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Or:

  Set Implicit Arguments.
  Definition id (t: Type) (l: list t) := l.
  Definition test := id (cons 1 nil).

On Sun, Oct 27, 2013 at 12:14:10AM +0200, Ilmārs Cīrulis wrote:
> Okay, it seems that curly braces is enough:
> Definition id {t:Type} (l: list t) := l.
> 
> Sorry for the disturbance.
> 
> 
> On Sun, Oct 27, 2013 at 12:47 AM, Ilmārs Cīrulis
> <ilmars.cirulis AT gmail.com>wrote:
> 
> > Let's suppose that I'm too lazy and want to use the function
> > Definition id (t: Type) (l: list t) := l
> > in lazy way:
> > Definition test := id (cons 1 nil)
> > (without argument t, because it can be found from the type of the list)
> >
> > How can I make it in such way, if possible?
> >

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/