coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.
Date: Mon, 30 May 2011 11:55:11 +0300
Header: best read with a sniffer

On Sun, May 29, 2011 at 04:20:40PM +0300, Georgi Guninski wrote:
> On Sun, May 29, 2011 at 04:14:45PM +0300, Georgi Guninski wrote:
> >
> > I have problem getting a real contradiction though.
> >
> > Attached is source code.
> >
>

Inductive t : Type := FUCKMS : t.
(* ^ like True *)
Definition expr2 (v:t) : Type := False.
Coercion expr2: t >-> Sortclass.

Lemma l1: exists a : t, a->False.
Proof.
eexists.
instantiate(1:=FUCKMS). (* wtf, don't really need this*)
compute. trivial.
Qed.

[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