Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (9 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

File:
1 edited

Legend:

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

    r246 r248  
    1 include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
    2 include "Programming/Datatypes/Compare.ma".
    3 include "Programming/Datatypes/Bool.ma".
    4 include "Programming/Datatypes/Maybe.ma".
     1include "BitVector.ma".
     2include "Compare.ma".
     3include "Bool.ma".
     4include "Maybe.ma".
    55
    66ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝
     
    9292nqed.
    9393
    94 ncheck length.
    95 
    9694(*
    9795nlemma test:
     
    104102  #N H V IH.
    105103  ncases H.
    106 *)
    107104
    108105nlemma insert_lookup_leaf:
     
    118115  @.
    119116  #N H V IH.
     117*)
Note: See TracChangeset for help on using the changeset viewer.