coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Randy Pollack <rpollack AT inf.ed.ac.uk>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Problem using Lemma as a coercion
- Date: Sun, 12 Jun 2011 10:51:39 -0400
Randy Pollack wrote:
BTW, I guess coercions are required for large scale formal
mathematics. For example, subtyping of algebraic structures by purely
structural means (fewer components, ...) is inadequate for real
mathematics.
I'm willing to believe that's true. I would still expect that program verification can get on pretty well with no coercions, type classes, setoids, or other sources of fanciness. ;)
- [Coq-Club] Problem using Lemma as a coercion, Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Randy Pollack
- Re: [Coq-Club] Problem using Lemma as a coercion, Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion, Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion, Jean-Francois Monin
- Re: [Coq-Club] Problem using Lemma as a coercion,
Randy Pollack
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
Archive powered by MhonArc 2.6.16.