Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem using Lemma as a coercion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem using Lemma as a coercion


chronological Thread 
  • 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. ;)



Archive powered by MhonArc 2.6.16.

Top of Page