The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Oh, but you also want the equality lemma.

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.

-- 
JH


Le 24/02/2016 14:30, Jacques-Henri Jourdan a écrit :
> Can't you use something like:
>
> Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang 
> Σ.
>   refine(auth_own heap_name {[ l := Excl v ]}).
> Qed.
>

Attachment: signature.asc
Description: OpenPGP digital signature