Hi, I am new to HOL. I was reviewing the wordsTheory and having a primary background in PVS, I was wondering if there is something in the pre-existing theories that says the following about bitvector concatanation
given two words, bvm: bitvector of size m bvn: bitvector of size n w2n (bvm @@ bvn) = w2n (bvm)*2**m + w2n(bvn) This of course assumes that we are not considering two's complementation. If we did the result would be different. Thanks, Nikhil ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
