coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Working with the Equivalence type class

From: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>
To: Brian Aydemir <baydemir AT cis.upenn.edu>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Working with the Equivalence type class
Date: Thu, 19 Mar 2009 17:51:02 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Le 19 mars 09 � 17:28, Brian Aydemir a �crit :

Hi all,

Hi Brian,

Is there a simple explanation for the behavior of these tactics in this
particular situation? When the equivalence relation I work with is
[eq], as it is in the above example, it would be nice if "===" was
treated the same as "=".

It is simply because [subst] uses a purely syntactic check for an
application of [eq] or [identity]. I guess upgrading it to work
up-to conversion would not cause major compatibility problems.
-- Matthieu

[Coq-Club] Working with the Equivalence type class, Brian Aydemir
- Re: [Coq-Club] Working with the Equivalence type class, Matthieu Sozeau