coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving equality of records

From: AUGER Cédric <sedrikov AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: Alexander Katovsky <apk32 AT cam.ac.uk>, coq-club AT inria.fr
Subject: Re: [Coq-Club] proving equality of records
Date: Tue, 17 Jul 2012 23:38:52 +0200

Another workaround is to provide an equivalence relation between
categories, and then just show that Op(Op C)~C instead of equality.

There is the setoid module in the coq standard library which provides a
lot of stuff to ease rewritings.

[Coq-Club] proving equality of records, Alexander Katovsky, 07/17/2012
- Re: [Coq-Club] proving equality of records, Jason Gross, 07/17/2012
  - Re: [Coq-Club] proving equality of records, AUGER Cédric, 07/17/2012