The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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.

Kind regards,
Ralf