coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variables outside sections

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Variables outside sections
Date: Fri, 4 Mar 2016 11:48:24 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f48.google.com
Ironport-phdr: 9a23:u0oSrhwLwjVtrk3XCy+O+j09IxM/srCxBDY+r6Qd0ekfIJqq85mqBkHD//Il1AaPBtWEra0awLqK+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU0Jr8h7z60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWbwyJ72ccW2NethdJHQXD8FmuXJD3syj3sudw8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

On 03/04/2016 11:33 AM, Igor Zhirkov wrote:

Jonathan, it does indeed.

To be fair, this works as well:

Definition my_struct : mixin_of cT :=
match cT as x return mixin_of x with
| Pack _ c => c
end.

By the way, the trick to finding these is proof mode:

Definition my_struct : mixin_of cT.
destruct cT. (*or case cT; intros *)
assumption.
Defined.

Print my_struct.

For those of us who find the peculiarities of directly using Gallina's match construct just too confusing for anything but the most trivial cases, the case analysis tactics (destruct, case, inversion, etc), plus Print can provide the solutions, if not the explanations.

-- Jonathan

[Coq-Club] Variables outside sections, Igor Zhirkov, 03/04/2016
- Re: [Coq-Club] Variables outside sections, Pierre-Marie Pédrot, 03/04/2016
- Re: [Coq-Club] Variables outside sections, Jonathan Leivent, 03/04/2016
  - Re: [Coq-Club] Variables outside sections, Igor Zhirkov, 03/04/2016
    - Re: [Coq-Club] Variables outside sections, Jonathan Leivent, 03/04/2016
  - Re: [Coq-Club] Variables outside sections, Pierre-Marie Pédrot, 03/04/2016