coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Bug of Feature?

From: David Leduc <david.leduc6 AT googlemail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Bug of Feature?
Date: Sat, 25 Sep 2010 07:13:59 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type :content-transfer-encoding; b=x+EayHloB9UyUJ+F7Odo2w83/tOToRnFeRWo9MXNpx07sJ+krQ7Ic67pmiNvTnJIwH Rtzoks7WCRp1yvzgxt9Bt/Rq6O7qQ0k1jnuNbQhE7SlTPTAetZ/JIy6TAzJOd0PVfRiu E6PZFIhkcjWJA/uVOEiEHVuU9fcGNgoqnuJkE=

Hi again,

Nobody seems to know about this feature/bug.
If it is a feature then it is not documented (as far as I understand
the reference manual).
If it is a bug then it is a useful one.

On Mon, Sep 20, 2010, I wrote:
> Record T : Type := {
> �carrier : Set ;
> �op : carrier -> carrier -> carrier
> }.
>
> Check fun (t:T)(x y:carrier t), op _ x y.
>
> (*
> Above, the implicit argument is inferred to be t.
> But there are other legal choices such as below.
> On which bases Coq chooses?
> *)
>
> Check fun (t:T)(x y:carrier t), op {| carrier := carrier t ; op := fun
> x y => x |} x y.
>

[Coq-Club] Bug of Feature?, David Leduc
- <Possible follow-ups>
- Re: [Coq-Club] Bug of Feature?, Hugo Herbelin