The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hi Arnaud,

For Ralf's purpose the generated term should be Opaque. As far as I see, 
one can only control the opacity of the equality lemma. So, given:

  Derive f SuchThat (f = λ x : nat, 10) As foo.

One can control whether foo is Opaque by ending the proof with 
Qed/Defined, but not whether f is Opaque.

Robbert

On 02/24/2016 09:15 PM, Arnaud Spiwack wrote:
> See also :
> https://coq.inria.fr/distrib/current/refman/Reference-Manual033.html#hevea_command305
>
> (syntax subject to changes by the time of next release)
>
> On 24 February 2016 at 14:57, Jacques-Henri Jourdan
> <jacques-henri.jourdan AT inria.fr
>  
> <mailto:jacques-henri.jourdan AT inria.fr>>
> wrote:
>
>     Le 24/02/2016 14:51, Ralf Jung a écrit :
>     > Hi,
>     >
>     >> Oh, but you also want the equality lemma.
>     > Right :)
>     >
>     >> Then you can do something like:
>     >>
>     >> Definition x : nat := 1.
>     >>
>     >> Definition x_aux : { x':_ & x' = x }.
>     >>   exact (existT _ _ eq_refl). Qed.
>     >> Definition x_sealed := projT1 x_aux.
>     >> Definition x_sealed_eq : x_sealed = x := projT2 x_aux.
>     >>
>     >> Which is, I admit, not ideal from a syntactic point of view. However,
>     >> note that the type and definition of x appear only once.
>     > Thanks, this indeed looks nicer than using modules!
>     >
>     > Unfortunately, if the type of x is more complicated, this loses all the
>     > information about implicit arguments: If some arguments of "x" were made
>     > implicit by putting them in "{...}", these are all explicit for
>     > x_sealed. So the type has to be repeated, or at least the implicitness
>     > information has to be declared again with Arguments.
>
>     Well, you don't really need x, so you don't need to give this
>     information twice. But yes, you have to repeat the information about
>     implicitness of arguments.
>
>      > Kind regards,
>      > Ralf