coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axiom setoideq_eq inconsistent?

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

[Coq-Club] Axiom setoideq_eq inconsistent?, Robin Green
- Re: [Coq-Club] Axiom setoideq_eq inconsistent?, Matthieu Sozeau
  - [Coq-Club] code duplication in ConCaT bcz of universe clash, Benedikt . AHRENS
    - Re: [Coq-Club] code duplication in ConCaT bcz of universe clash, Hugo Herbelin