Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unexpected axiom in extraction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unexpected axiom in extraction


chronological Thread 
  • 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].



Archive powered by MhonArc 2.6.16.

Top of Page