Ignore:
Timestamp:
Nov 11, 2010, 12:27:04 PM (9 years ago)
Author:
mulligan
Message:

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File:
1 edited

Legend:

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

    r230 r231  
    3131  λc: BitVector n.
    3232    zip Bool Bool Bool n exclusive_disjunction b c.
     33
     34nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝
     35       
Note: See TracChangeset for help on using the changeset viewer.