coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.

From: Adam Chlipala <adam AT chlipala.net>
To: Georgi Guninski <guninski AT guninski.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.
Date: Mon, 30 May 2011 07:36:54 -0400

It's not clear to me why these examples are interesting. I don't see any argument here for why Coq should behave differently in any respect.

Also, I expect some readers of the list would appreciate it if you refrained from using profanity in choosing identifiers for examples. ;)

[Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
- Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
  - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
  - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
    - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Adam Chlipala
    - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Brandon Moore
      - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
        
        Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Adam Chlipala
        
        Weak Pollack-super-inconsistency [Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.], dhr. dr. J McKinna
        
        Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Georgi Guninski
        
        Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Brandon Moore
        
        Re: [Coq-Club] Abuse of coercions gives weird results in coqtop., Brandon Moore