coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] congruence
Date: Wed, 30 Sep 2015 13:43:18 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mta02.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta03.in.vera.com.uy ACA12226C0C
Ironport-phdr: 9a23:2JhhBRyDQLyQHDfXCy+O+j09IxM/srCxBDY+r6Qd0eMWIJqq85mqBkHD//Il1AaPBtWHrawdwLSL+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStKU0Z38ib360qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGxav/sq9IZNVKz7e+w0SrlRDTJ0LW0v7YvgshyFUBrHpiBECiRF2iZPVgPC9VTxWor7+n/xsfM40y2HN+X3S6o1UHKs9fE4ZgXvjXI/PiIj8WrWg4RIgbhSvA6m70hn2JbZeoiJKP1WYK7HdJURQm8HQ9cHBH8JOZ+1c4ZaVrlJBu1ftYSo/ANWoA==

I need to use congruence of equality.

I import the files Logic and Logic_Type

but does not find it. (I want to use the

function congr_id).

Is it in another place?

Regards

Patricia Peratto

[Coq-Club] congruence, Patricia Peratto, 10/01/2015
- Re: [Coq-Club] congruence, Laurent Thery, 10/01/2015