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

Re: question about prove


I don't get any TCCs when typechecking your theory fragment: (PVS Version 2.3
(patch level

subrina: theory begin

dd: TYPE = {r: real | r>=0}containing 1
ii: TYPE = posnat
a: TYPE = [# pr: dd,
             bk: dd #]

aa: TYPE = ARRAY[posnat -> a]

m: ii
i: posnat
T: aa

end subrina

I suggest that you examine the col/line numbers given with the TCC,
the TCC may occur elsewhere in your file.

(typepred "pr(T(i!1))" "bk(T(i!1))") might also help.

Hope that helps...
  Christoph Berg
cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
Office +49/681/302-4129, Fax -4290, Home +49/681/9657944
Computer Science Dept., Universität des Saarlandes, Saarbrücken

PGP signature