Ignore:
Timestamp:
Nov 11, 2010, 4:56:59 PM (9 years ago)
Author:
mulligan
Message:

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File:
1 edited

Legend:

Unmodified
Added
Removed

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

    r231 r232  
    3232    zip Bool Bool Bool n exclusive_disjunction b c.
    3333
    34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝
     34nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝
     35  match m with
     36    [ Z ⇒ ?
     37    | S o ⇒ ?
     38    ].
     39   
     40    //.
     41nqed.
     42
     43ncheck pad.
    3544       
Note: See TracChangeset for help on using the changeset viewer.