Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Running computations inside Coq

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Running computations inside Coq


Chronological Thread 
  • From: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] Running computations inside Coq
  • Date: Wed, 10 Feb 2016 08:54:35 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:lm7AiRBTPiLtWmuZAyeSUyQJP3N1i/DPJgcQr6AfoPdwSP7+p8bcNUDSrc9gkEXOFd2CrakU1KyN6uu5ADBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbpotaKOlkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kr8jV7FWCDktL0gw/9eutB/ZTALJ530GU2xQnAAbLRLC6UTXWI3wuSyyiuNmwyjSacDwV7E/XnK+5rxwSTfpjj0GPng36jeE2YRLkKtHrUf59FREyInObdTNOQ==

On Wed, Feb 10, 2016 at 08:38:04AM +0100, Ralf Jung wrote:
> > Definition master_key : unit := tt.
> > Global Opaque master_key.
>
> but I do not know if this has any undesired side-effects.

Unfortunately the opacity provided by "Opaque" is not as strong as the
one provided by "Qed". Opaque is a directive honoured by some Coq
tactics and it is just a hint to the kernel. The kernel would happily
unfold constants declared as Opaque, but would not unfold constants
that are Qed-opaque.

The point of locking constants is mostly to circumvent performance
issues in the kernel. Hence your solution would make the system
terribly slow (i.e. diverging).

Best,
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page