ssreflect - Re: [ssreflect] Running computations inside Coq

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Running computations inside Coq

From: Ralf Jung <>
To:
Subject: Re: [ssreflect] Running computations inside Coq
Date: Wed, 10 Feb 2016 08:38:04 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:J2xUBha5bS506mNntjeB727/LSx+4OfEezUN459isYplN5qZpci4bnLW6fgltlLVR4KTs6sC0LqJ9fu5EjVZuN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcaKKFwR3XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtVqdCAToiPmspzMjwr1zCSxGO7z0dVH8Xm1xGGVvr9hb/C634tiWylPd712HOP9DwQpgxQTXn9LhwDhjyh3FUZHYC7GjLh5ko3+pgqxW7qkknzg==

Hi,

> On 02/06/2016 11:54 AM, Felipe Cerqueira wrote:
>> Let l := [:: 1; 2; 3].
>> Eval compute in (\sum_(x <- l) x).
>
>
> Yep unfortunately for you the bigop operator is locked, in order to
> compute, you have to explicitly unlock it.

If ssreflect would define the "master_key" transparently, and only then
make it opaque with a separate command, it would be possible to do
"Local Opaque master_key" before doing computation. Wouldn't that solve
the problem here?

Essentially, I am suggesting to replace

> Lemma master_key : unit. Proof. exact tt. Qed.

by

> Definition master_key : unit := tt.
> Global Opaque master_key.

but I do not know if this has any undesired side-effects.

Kind regards,
Ralf

[ssreflect] Running computations inside Coq, Felipe Cerqueira, 02/05/2016
- Re: [ssreflect] Running computations inside Coq, Emilio Jesús Gallego Arias, 02/06/2016
  - Re: [ssreflect] Running computations inside Coq, Felipe Cerqueira, 02/06/2016
    - Re: [ssreflect] Running computations inside Coq, Laurent Thery, 02/06/2016
      - Re: [ssreflect] Running computations inside Coq, Ralf Jung, 02/10/2016
        
        Re: [ssreflect] Running computations inside Coq, Enrico Tassi, 02/10/2016
    - Re: [ssreflect] Running computations inside Coq, Emilio Jesús Gallego Arias, 02/06/2016

List archive

Re: [ssreflect] Running computations inside Coq