Ignore:
Timestamp:
Nov 23, 2010, 12:56:26 PM (9 years ago)
Author:
mulligan
Message:

Need stronger set_ and get_index functions on vectors (current ones return a Maybe type).

File:
1 edited

Legend:

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

    r258 r259  
    44
    55(* include "ASM.ma". *)
     6include "Arithmetic.ma".
    67include "BitVectorTrie.ma".
    7 include "Arithmetic.ma".
    88
    99ninductive SFR8051: Type[0] ≝
     
    8585}.
    8686
     87alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)".
    8788
     89ndefinition set_8051_sfr ≝
     90  λs: Status.
     91  λi: SFR8051.
     92  λb: Byte.
     93    let index ≝ sfr_8051_status i in
     94    let
    8895
    8996ndefinition initialise_status ≝
    90   mk_Status
    91     (Stub Byte sixteen)
    92     (Stub Byte seven)
    93     (Stub Byte seven)
    94     (Stub Byte sixteen)
    95     (zero sixteen)
    96     ([ zero eight; zero eight; zero eight; zero eight;
    97        zero eight; zero eight; zero eight; zero eight ]).
     97  let status ≝ mk_Status (Stub Byte sixteen)
     98                         (Stub Byte seven)
     99                         (Stub Byte seven)
     100                         (Stub Byte sixteen)
     101                         (zero sixteen)
     102                         (replicate Byte nineteen (zero eight))
     103                         (replicate Byte five (zero eight)) in
     104  status.
Note: See TracChangeset for help on using the changeset viewer.