Changeset 266


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

Changes to bitvector.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

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

    r263 r266  
    3333  λb: BitVector n.
    3434  λm: Nat.
    35     get_index Bool n b m.
     35  λp: m < n.
     36    get_index Bool n b m p.
    3637   
    3738interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
     
    4142  λb: BitVector n.
    4243  λm: Nat.
    43     set_index_weak Bool n b m.
     44  λp: m < n.
     45  λc: Bool.
     46    set_index_weak Bool n b m c.
    4447   
    4548ndefinition drop ≝
  • Deliverables/D4.1/Matita/Interpret.ma

    r265 r266  
    221221  λs: Status.
    222222    let sfr ≝ special_function_registers_8051 s in
    223     let psw ≝ get_index … (get_8051_index SFR_PSW) s ? in
     223    let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in
    224224      get_index … Z psw ?.
    225225               
  • Deliverables/D4.1/Matita/Vector.ma

    r265 r266  
    8383interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    8484
    85 (*
    8685nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8786  (match m with
     
    10099    nassumption.
    101100nqed.
    102 *)
    103101   
    104102nlet rec set_index_weak (A: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.