coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Subtyping and sig.

From: J�r�mie Koenig <jk AT jk.fr.eu.org>
To: Guillaume Yziquel <guillaume.yziquel AT citycable.ch>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Subtyping and sig.
Date: Wed, 22 Feb 2012 00:21:42 +0100
Authentication-results: mr.google.com; spf=pass (google.com: domain of jeremie.koenig AT gmail.com designates 10.50.161.170 as permitted sender) smtp.mail=jeremie.koenig AT gmail.com; dkim=pass header.i=jeremie.koenig AT gmail.com

Hi,

On Tue, Feb 21, 2012 at 10:07 PM, Guillaume Yziquel
<guillaume.yziquel AT citycable.ch>
wrote:
> How do you deal with 'subtyping' when using the { .. | .. } notation?

Besides doing things manually or with coercions, you may want to check
out "Program" [1].

[1] http://coq.inria.fr/doc/Reference-Manual028.html

--
J�r�mie Koenig
<jk AT jk.fr.eu.org>
http://jk.fr.eu.org/

[Coq-Club] Subtyping and sig., Guillaume Yziquel
- Re: [Coq-Club] Subtyping and sig., gallais @ ensl.org
  - Re: [Coq-Club] Subtyping and sig., Guillaume Yziquel
- Re: [Coq-Club] Subtyping and sig., J�r�mie Koenig
  - Re: [Coq-Club] Subtyping and sig., Guillaume Yziquel