coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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] Axiom setoideq_eq inconsistent?, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.