Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Feature Request: Sealed definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Feature Request: Sealed definitions


Chronological Thread 
  • From: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Feature Request: Sealed definitions
  • Date: Wed, 24 Feb 2016 14:52:10 +0100

You can even simplify it a little bit by inlining the definition of x:

Definition x_aux : { x':_ & x' = 1 }.
exact (existT _ _ eq_refl). Qed.
Definition x_sealed := projT1 x_aux.
Definition x_sealed_eq : x_sealed = _ := projT2 x_aux.

Le 24/02/2016 14:43, Jacques-Henri Jourdan a écrit :
> 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.
>


Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page