coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Russell O'Connor" <roconnor AT Math.Berkeley.EDU>
- To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Reducing memory usage
- Date: Thu, 9 Jan 2003 15:29:40 -0800 (PST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
[To:
coq-club AT pauillac.inria.fr]
On Wed, 8 Jan 2003, Judicael Courant wrote:
> I guess the problem Pierre mentions is about implicit universes.
Ahh, I figured as much, but didn't immediately see how to do it. Thanks.
I guess having the n in Type_n be implicit is a design flaw in Coq. Good
to know for future proof systems.
- --
Russell O'Connor <http://www.math.berkeley.edu/~roconnor/>
``[Law enforcement officials] suggested that the activists were stopped
not because their names are on the list, but because their names resemble
those of suspected criminals or terrorists.'' -- SFGate.com
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)
iQCVAwUBPh4F6E0+aO5oRkNZAQIhrwP/axwt/5IB0VkJgWXyvD4LrVTZYTOpClup
9r0nkO47s3V9ngZgeaBoxgFcAp/c2jt86ikBHK7pxS5iLUys4UrpzmJVLvh9B0mi
wl3ix/8GjoYbk7+1rLvuuC+/RcWeAvLp0oNLY+kcilZ8Vu3YND45GVYpUXNTVjIU
XSc5goZPzXM=
=CrBf
-----END PGP SIGNATURE-----
- Re: [Coq-Club] Reducing memory usage, Pierre Courtieu
- Re: [Coq-Club] Reducing memory usage,
Russell O'Connor
- Re: [Coq-Club] Reducing memory usage,
Judicael Courant
- Re: [Coq-Club] Reducing memory usage, Russell O'Connor
- Re: [Coq-Club] Reducing memory usage,
Judicael Courant
- Re: [Coq-Club] Reducing memory usage,
Russell O'Connor
Archive powered by MhonArc 2.6.16.