coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why identity coerions?

From: Victor Porton <porton AT narod.ru>
To: coq-club AT inria.fr
Subject: [Coq-Club] Why identity coerions?
Date: Fri, 04 Nov 2011 03:36:59 +0400
Envelope-from: porton AT yandex.ru

Honestly I haven't quite understood what are identity coercions.

Most important I don't understand what is the purpose of identity coercions.
Why we need special identity coercions, not just plain coercions?

--
Victor Porton - http://portonvictor.org

[Coq-Club] Why identity coerions?, Victor Porton
- <Possible follow-ups>
- Re: [Coq-Club] Why identity coerions?, Paolo Herms
  - Re: [Coq-Club] Why identity coerions?, Victor Porton