coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: frank maltman <frank.maltman AT googlemail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Unexpected axiom in extraction
- Date: Sat, 06 Aug 2011 10:08:31 -0400
frank maltman wrote:
Module Type TEST.
Parameter foo : nat.
End TEST.
Module Test : TEST.
Axiom foo : nat.
Extract Inlined Constant foo => "prim_foo".
End Test.
Axiom bar : nat.
Extract Inlined Constant bar => "prim_bar".
Definition x := Test.foo + bar.
--8<--
$ coqc Test.v
$ coq
< Require Test.
< Extraction Library Test.
[...]
Note that, now, Test.foo is an unrealized axiom!
That makes sense to me. It's an unrealized axiom in Coq, too! It seems entirely consistent with opaque signature ascription that the [Extract Inlined] command is hidden to code outside [Test], since it doesn't appear in [TEST].
- [Coq-Club] Unexpected axiom in extraction, frank maltman
- Re: [Coq-Club] Unexpected axiom in extraction, Adam Chlipala
Archive powered by MhonArc 2.6.16.