[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

duplicate declarations deemed ambiguous



I'm working on development tools for Extended ML
(www.dcs.ed.ac.uk/home/dts/eml/) and am using PVS as the backend.  At one
point a naive translation of EML into PVS yields the following two
declarations (the first stems from a signature, the second from a
structure).  

a : int
a : int = 5

PVS rejects this with "a has previously been declared with type int, which
is ambiguous".  

Why?  Is it because the first wants a to be uninterpreted, but the second
says a is definitely 5?

It's not difficult to get out of this hole, but why is it there?

Ben Kleinman
bkleinman@writeme.com
http://www.dcs.ed.ac.uk/home/bkk