coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Axiom setoideq_eq inconsistent?

From: Robin Green <greenrd AT greenrd.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Axiom setoideq_eq inconsistent?
Date: Wed, 10 Feb 2010 11:10:30 +0000
Organization: Swansea University

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?
--
Robin

[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