coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Feature Request: Sealed definitions, (continued)
- Re: [Coq-Club] Feature Request: Sealed definitions, Jeehoon Kang, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Robbert Krebbers, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Ralf Jung, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Arnaud Spiwack, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Robbert Krebbers, 02/25/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Arnaud Spiwack, 02/25/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Robbert Krebbers, 02/25/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Ralf Jung, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jacques-Henri Jourdan, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Robbert Krebbers, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Ralf Jung, 02/24/2016
- Re: [Coq-Club] Feature Request: Sealed definitions, Jeehoon Kang, 02/24/2016
Archive powered by MHonArc 2.6.18.