[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
a : int
a : int = 5
PVS rejects this with "a has previously been declared with type int, which
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?