coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]How can I make the definitions in my Modules more transparent?, mulhern
Archive powered by MhonArc 2.6.16.