Changeset 744 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r726 r744  
    4040definition pad ≝
    4141  λm, n: nat.
    42   λb: BitVector n.
    43     let padding ≝ replicate bool m false in
    44       append bool m n padding b.
     42  λb: BitVector n. pad_vector ? false m n b.
    4543     
    4644(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.