coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Extract Constant" inside a parameterised module

From: Keiko Nakata <keiko.nakata AT FireEye.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] "Extract Constant" inside a parameterised module
Date: Thu, 19 Nov 2015 09:18:00 +0000
Accept-language: en-GB, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=keiko.nakata AT FireEye.com; spf=Pass smtp.mailfrom=keiko.nakata AT fireeye.com; spf=None smtp.helo=postmaster AT esa2.fireeye.iphmx.com
Domainkey-signature: s=corporate; d=fireeye.com; c=nofws; q=dns; h=X-IronPort-AV:Received:Received:From:To:Subject: Thread-Topic:Thread-Index:Date:Message-ID:Accept-Language: Content-Language:X-MS-Has-Attach:X-MS-TNEF-Correlator: x-originating-ip:Content-Type:Content-ID: Content-Transfer-Encoding:MIME-Version; b=aOjTt9EySq1MQjkgN4zIKYSczT0Rx102QC7yavoDres4r4o/c6Vbqp/d /Ge3QoFk9nNfWbbal1b/eALx4ItJLol67Cl1hIERDDEtCGfu1lEVS74Ku BwYYNk6DJuiHvEzJgVelRoH0UO2e2BqbafFFpCR8mvUhUSU6J7tM3Ip5V c=;
Ironport-phdr: 9a23:hAkE0xyJKE922qDXCy+O+j09IxM/srCxBDY+r6Qd0ewSIJqq85mqBkHD//Il1AaPBtWGrawewLOM4+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6PyZrtnLnoq9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6vled82y7SG8T1RKw9EWCh4qZoT1nugSQOKzcR3mDNh+FhgeRQpxf39E83+JLdfIzAbKk2RajaZ95PHWc=

Hi,

I have a problem in realising axioms inside functors.
"Extract Constant" is ignored when inside a functor.

---

Module N (X:A).
Parameter n : bool.
(* Does not work *)
Extract Constant n => "true".
End N.

Module A_1.
Definition a := true.
End A_1.

Module NA_1 := N A_1.

(* Does not work either *)
Extract Constant NA_1.n => "true".

---

I wonder if I am missing something?

Best regards,
Keiko

This email and any attachments thereto may contain private, confidential,
and/or privileged material for the sole use of the intended recipient. Any
review, copying, or distribution of this email (or any attachments thereto)
by others is strictly prohibited. If you are not the intended recipient,
please contact the sender immediately and permanently delete the original and
any copies of this email and any attachments thereto.

[Coq-Club] "Extract Constant" inside a parameterised module, Keiko Nakata, 11/19/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] "Extract Constant" inside a parameterised module, Keiko Nakata, 11/19/2015