Ignore:
Timestamp:
Nov 22, 2010, 10:05:05 AM (9 years ago)
Author:
mulligan
Message:

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

File:
1 edited

Legend:

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

    r244 r246  
    66include "Util.ma".
    77
    8 include "logic/pts.ma".
     8include "Universes.ma".
    99
    1010include "Nat.ma".
    11 
    1211include "List.ma".
    13 
    1412include "Cartesian.ma".
    1513
    16 include "Plogic/equality.ma".
     14include "Equality.ma".
    1715
    1816(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    9694(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9795(* Folds and builds.                                                          *)
    98 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     96(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9997   
    10098nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
     
    292290    reverse A n (shift_left_1 A n (reverse A n v) a).
    293291   
    294 ncheck Nat.
    295    
    296292ndefinition shift_left ≝
    297293  λA: Type[0].
Note: See TracChangeset for help on using the changeset viewer.