Ignore:
Timestamp:
Nov 23, 2010, 4:43:34 PM (9 years ago)
Author:
sacerdot
Message:
  • use standard notation for exponential
  • Bit is now Bool
File:
1 edited

Legend:

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

    r262 r263  
    1818
    1919ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    20 ndefinition Bit ≝ BitVector (S Z).
     20ndefinition Bit ≝ Bool.
    2121ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
    2222ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
Note: See TracChangeset for help on using the changeset viewer.