coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A fast "eq" predicate for Gallina?
- Date: Wed, 20 Jan 2021 21:22:38 +0100
On 20/01/2021 21:17, jonikelee AT gmail.com wrote:
> I am working on some Coq reflection procedures and trying to stay
> within Gallina as much as possible.
Why don't you implement your own heap inside Coq then, using some form
of state monad? It's going to be overly cumbersome but at least you'd
get pointer equality from first principles.
PMP
Attachment:
OpenPGP_signature
Description: OpenPGP digital signature
- [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Sylvain Boulmé, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Jean-Christophe Léchenet, 01/21/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Adam Chlipala, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Sylvain Boulmé, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Pierre-Marie Pédrot, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Xavier Leroy, 01/21/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/21/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Xavier Leroy, 01/21/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Pierre-Marie Pédrot, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Pierre-Marie Pédrot, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Adam Chlipala, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Mario Carneiro, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Mario Carneiro, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Sylvain Boulmé, 01/20/2021
Archive powered by MHonArc 2.6.19+.