coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Sigma Type Coercion

From: Julio <coquser AT googlemail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Sigma Type Coercion
Date: Wed, 9 Sep 2009 12:01:39 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=IGq9EcANiErNzHY0gY+78DevTlYNXAqAD72aAG1unneAtu5AS6O8R7h9zftK8j6iQb p2/vnM1Qumb4UhmJkVju2jceBcXwj68XV/5d7OEr2QxwoG7Iy2hSq9vPRe9BiRtN/RSh AfvOU92+5cvc7eGHJqkwV12BM4oe7Adi38V+w=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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 ?*)

[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