Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A fast "eq" predicate for Gallina?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A fast "eq" predicate for Gallina?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.19+.

Top of Page