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

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

Location:
Deliverables/D4.1/Matita
Files:
4 added
6 edited

Legend:

Unmodified
Added
Removed

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

    r240 r246  
    66(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    77
    8 include "Universes/Universes.ma".
     8include "Universes.ma".
    99
    10 include "Datatypes/Listlike/Vector/Vector.ma".
    11 include "Datatypes/Listlike/List/List.ma".
    12 
    13 include "Datatypes/Nat/Nat.ma".
    14 include "Datatypes/Nat/Addition.ma".
    15 include "Datatypes/Nat/Division_Modulus.ma".
    16 include "Datatypes/Nat/Exponential.ma".
    17 
    18 include "Datatypes/Bool.ma".
     10include "Vector.ma".
     11include "List.ma".
     12include "Nat.ma".
     13include "Bool.ma".
    1914
    2015(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

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

    r232 r246  
    1 include "logic/pts.ma".
     1include "Universes.ma".
    22
    33ninductive Bool: Type[0] ≝

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

    r236 r246  
    1 include "logic/pts.ma".
     1include "Universes.ma".
    22
    33nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝

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

    r237 r246  
    55include "Bool.ma".
    66
    7 include "logic/pts.ma".
    8 include "Plogic/equality.ma".
    9 include "Plogic/connectives.ma".
     7include "Connectives.ma".
    108
    119(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

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

    r243 r246  
    1 include "logic/pts.ma".
    2 
    31include "Nat.ma".
    42

  • 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.