[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
a question about bitwise
I have a question about the bitwise operation in PVS. In the prelude file,
bvec: TYPE=[below(N)->bit] is defined in the theory "bv". Then in the
theory "bv_concat_def", the definition of "o" is:
(lambda(nm:below(n+m)):if nm<m then bvm(nm)
My question is:
What does "bvec[n]" mean? Does it mean an array of type "bvec"?
Thanks a lot.