coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Turn a definition opaque

From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turn a definition opaque
Date: Mon, 22 Apr 2019 19:51:57 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout10.partage.renater.fr

On Mon, Apr 22, 2019 at 7:34 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

Hi,

I am wondering if there a way to turn a definition entirely opaque, so that the type checker won't unfold it? I guess this question has been raised once a while but I cannot find a solution.

ssreflect has some tricks to help with this, see https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#locking-ssr

I, too, would like "Opaque" to completely hide the definition of a name, instead of just making it harder to unfold.

Best,

- Xavier Leroy

[Coq-Club] Turn a definition opaque, Jason -Zhong Sheng- Hu, 04/22/2019
- Re: [Coq-Club] Turn a definition opaque, Gaëtan Gilbert, 04/22/2019
- Re: [Coq-Club] Turn a definition opaque, Xavier Leroy, 04/22/2019
  - Re: [Coq-Club] Turn a definition opaque, Gert Smolka, 04/24/2019