coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Sigma Type Coercion

From: Julio <coquser AT googlemail.com>
To: Luke Palmer <lrpalmer AT gmail.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Sigma Type Coercion
Date: Wed, 9 Sep 2009 21:07:35 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=H5HTc9Ni09sX4x7rdDQUbEd0ygT+bddwXlvkScJa8/YLS+RUonJY0XvJkaWoIzSckB wk1Bhd1Xqr7WtZzI5NKxBwH5kb519JgJxrPXM1dA3yOEOeHVuAPHmcpOdsLZJj3OKJJL qsheM8rM2f4EGQ5rfymiEGzaW7WS+lKabMFKg=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm not sure what the rest of the definition Definition ASig_to_BSig : ASig -> BSig := ... should be.

On Wed, Sep 9, 2009 at 1:32 PM, Luke Palmer <lrpalmer AT gmail.com> wrote:

On Wed, Sep 9, 2009 at 5:01 AM, Julio <coquser AT googlemail.com> wrote:
> Is sigma type coercion possible?
>
> Require Import String.
> Open Scope string_scope.
> Record A:Set := {total:nat}.
> Record B:Set := {name:string}.
>
> (*Sigma types.*)
> Definition ASig := {a:A | (total a) > 10}.
> Definition BSig := {b:B | (name b) = "kilometers"}.
> (*Syntax for Coercion ASig >-> BSig ?*)

The same as all other coercions.

Definition ASig_to_BSig : ASig -> BSig := ...
Coercion ASig_to_BSig : ASig >-> BSig.

Luke

[Coq-Club] Sigma Type Coercion, Julio
- Re: [Coq-Club] Sigma Type Coercion, Luke Palmer
  - Re: [Coq-Club] Sigma Type Coercion, Julio
    - Re: [Coq-Club] Sigma Type Coercion, Adam Chlipala
      - Re: [Coq-Club] Sigma Type Coercion, Adam Chlipala