Ignore:
Timestamp:
Nov 10, 2010, 5:26:08 PM (9 years ago)
Author:
mulligan
Message:

Lots of work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r228 r230  
    44
    55ndefinition BitVector ≝ λn: Nat. Vector Bool n.
     6ndefinition Bit ≝ BitVector (S Z).
     7ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
     8ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
     9ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
     10ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
    611
    712ndefinition zero ≝
     
    2631  λc: BitVector n.
    2732    zip Bool Bool Bool n exclusive_disjunction b c.
    28    
    29    
Note: See TracChangeset for help on using the changeset viewer.