Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Axiom setoideq_eq inconsistent?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axiom setoideq_eq inconsistent?


chronological Thread 
  • From: Matthieu Sozeau <mattam AT mattam.org>
  • To: Robin Green <greenrd AT greenrd.org>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Axiom setoideq_eq inconsistent?
  • Date: Thu, 11 Feb 2010 10:45:04 -0500


Le 10 févr. 10 à 06:10, Robin Green a écrit :

Doesn't Axiom setoideq_eq in Coq.Classes.SetoidAxioms make Coq inconsistent?

Surely it would be better to have a parameter of the goal talking
about certain setoid(s), rather than an axiom?

Yes it is inconsistent and shouldn't be in the stdlib.
-- Matthieu



Archive powered by MhonArc 2.6.16.

Top of Page