coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: 回复: Re: [Coq-Club] usage of eq_ind

From: Roman Beslik <beroal AT ukr.net>
To: coq-club AT inria.fr
Subject: Re: 回复: Re: [Coq-Club] usage of eq_ind
Date: Fri, 28 May 2010 16:18:10 +0300
Disposition-notification-to: Roman Beslik <beroal AT ukr.net>

Hi. "x=y" (as type) is a set of proofs of the proposition "x=y", IMHO. Implication (as type constructor) constructs a set of functions that transform a proof into another proof in some way.

On 28.05.10 13:59, 许庆国 wrote:

What's meaning of the type "x=y" ? Is it a predication type over type A，or a Set type or the dependent product type?

Best regards,
  Roman Beslik.

[Coq-Club] usage of eq_ind, qgxu
- Re: [Coq-Club] usage of eq_ind, Adam Chlipala
- Re: [Coq-Club] usage of eq_ind, Pierre Casteran
- �ظ�: Re: [Coq-Club] usage of eq_ind, ��
  - Re: �ظ�: Re: [Coq-Club] usage of eq_ind, Pierre Casteran
  - Re: 回复: Re: [Coq-Club] usage of eq_ind, Roman Beslik