Ignore:
Timestamp:
Nov 12, 2010, 5:09:39 PM (11 years ago)
Author:
mulligan
Message:

More work on bitvectors.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/BitVector.ma

    r237 r238  
    6969  λb: BitVector n.
    7070    map Bool Bool n (negation) b.
     71
     72(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     73(* Rotates and shifts.                                                        *)
     74(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     75
     76ndefinition rotate_left ≝
     77  λm, n: Nat.
     78  λb: BitVector n.
     79    rotate_left Bool n m b.
     80
     81ndefinition rotate_right ≝
     82  λm, n: Nat.
     83  λb: BitVector n.
     84    rotate_right Bool n m b.   
    7185   
    7286(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.