coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] implicit argument in identity

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] implicit argument in identity
Date: Thu, 30 Jun 2011 13:58:46 -0400

Hello,

does anybody know where the first ( type ) argument of [ identity ] is
declared to be implicit ?

[ identity ] itself is defined in Coq.Init.Datatypes but there the first
argument is explicit.

Thanks!
Vladimir.

[Coq-Club] implicit argument in identity, Vladimir Voevodsky
- Re: [Coq-Club] implicit argument in identity, Pierre Courtieu
  - Re: [Coq-Club] implicit argument in identity, Vladimir Voevodsky