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

a question about bitwise



Hi,

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:

o(bvn:bvec[n], bvm:bvec[m]):bvec[n+m]=
  (lambda(nm:below(n+m)):if nm<m then bvm(nm)
                         else bvn(nm-m)
                         endif)

My question is:

What does "bvec[n]" mean? Does it mean an array of type "bvec"?

Thanks a lot.

Bin.