Skip to Content.
Sympa Menu

coq-club - [Coq-Club]How can I make the definitions in my Modules more transparent?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]How can I make the definitions in my Modules more transparent?


chronological Thread 
  • From: mulhern <mulhern AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]How can I make the definitions in my Modules more transparent?
  • Date: Tue, 11 Jul 2006 12:52:28 -0500
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=WCy5r0RZ5qMcC0wYWO8LMX7Gq8AOPKK0/4u29HkYlvLxxoJlEwWjc2CJf619k15mL5jEJ8ZPM8CmT3iOLVO7v6oNAFFnVAInLrBwgsGnE76vM1ZHETXOSU3ApxvGkWtr5gqSESVnM5a0FQDVdC8vnzw5OMOpwR24ROYRRx1fqFA=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi!

I'm doing a proof and I get this error.

Coq < Load reference.
Error while reading /Users/mulhern/mulhern/cs/pierce_test/reference.v :
File "/Users/mulhern/mulhern/cs/pierce_test/reference.v", line 229,
characters 39-54
Error:
In environment
eval : term * store -> term * store -> Prop
t : term
s : store
s' : store
H : isval t
The term "exist isval t H" has type "sig isval"
while it is expected to have type "Store.V"

But Store.V = sig isval as I can tell by this succession of Print statements.

Coq < Print Store.V
Coq < .
Store.V = ValExp.A
    : Set


Coq < Print ValExp.A.
ValExp.A = {t : term | isval t}
    : Set

How can I make the Coq compiler use that information which it so
clearly possesses?

Store looks like this:

Coq < Print Store.
Module Store
 : Sig
     Definition V
     ....
     Definition allocate
   End
 := (Map_Wf_Ext Val)

ValExp looks like this:

Coq < Print ValExp.
Module ValExp
 : Sig
     Definition A
     Definition equal
     Parameter equal_refl
     Parameter equal_sym
     Parameter equal_trans
     Parameter equal_dec
   End
 := Struct
      Definition A
      Definition equal
      Theorem equal_refl
      Theorem equal_sym
      Theorem equal_trans
      Theorem equal_dec
    End

Map_Wf_Ext looks like this:

Coq < Print Map_Wf_Ext.
Module Map_Wf_Ext
 : Funsig (Val : VALUE)
     Sig
       Definition V
       ...
       Definition allocate
     End
 := Functor [Val:VALUE]
      Struct
        Definition V
        ....
        Definition allocate
      End

And VALUE looks like this.

Coq < Print VALUE.
Module Type VALUE = Sig
                     Parameter A
                     Parameter equal
                     Parameter equal_dec
                     Parameter equal_refl
                     Parameter equal_sym
                     Parameter equal_trans
                   End

-mulhern





Archive powered by MhonArc 2.6.16.

Top of Page