The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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> 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