Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Dependent Equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dependent Equality


chronological Thread 
  • From: "Russell O'Connor" <roconnor AT Math.Berkeley.EDU>
  • To: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Dependent Equality
  • Date: Tue, 1 Jul 2003 16:44:59 -0700 (PDT)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

Can someone explain to me the conditions neccesary on the Goal in order
for Dependent Rewrite to work?

- -- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)

iQCVAwUBPwIdBU0+aO5oRkNZAQIaQwQAqIrLDoacGLUgg8IIlIFjASkRYAALAcFE
ou6QAXQKsdU7FT2uxXbDS2CCiUwivLf+896hAhLtsPnGUV1P5+ubHYiN1pvz6g1D
bQNFgR3AQ45tjOqXl87VMnBUWpQdvGiQtJwNqT0yy6s0YbcPCEfHuBD1ejNPZWFI
CRb5BLGcWSw=
=qt1Y
-----END PGP SIGNATURE-----





Archive powered by MhonArc 2.6.16.

Top of Page