coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interaction of coercions and definitions

From: "Mark Dickinson" <dickinsm AT gmail.com>
To: "Georges Gonthier" <gonthier AT microsoft.com>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Interaction of coercions and definitions
Date: Thu, 23 Oct 2008 13:01:47 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=Xy3xLD3u5QU5+JjntoDeahD6eWDwr7ZcRu/ry7s75sgqcDVca61zBQHnIM6fITF21A 9WIea3V5oXMG+olMEa1/8NHnKs/juYQeINCw7mHakuDX5YS/E7dAAPrvTBg7HvmqzisL 9r4T1Z2kkPh1WzMXyT8Dg7II0fBmxb2ogmfRw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Oct 23, 2008 at 12:47 PM, Georges Gonthier
<gonthier AT microsoft.com>
wrote:

> the declaration
> Identity Coercion fun_of_relation : relation >-> Funclass.
> will sort the problem out (it tells the coercion system that relation is an
> alias for a function type).

Many thanks---that was exactly what I was missing!

Mark

[Coq-Club] Interaction of coercions and definitions, Mark Dickinson
- RE: [Coq-Club] Interaction of coercions and definitions, Georges Gonthier
  - Re: [Coq-Club] Interaction of coercions and definitions, Mark Dickinson
- Re: [Coq-Club] Interaction of coercions and definitions, Vladimir Komendantsky