Changeset 259 for Deliverables
 Timestamp:
 Nov 23, 2010, 12:56:26 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r258 r259 4 4 5 5 (* include "ASM.ma". *) 6 include "Arithmetic.ma". 6 7 include "BitVectorTrie.ma". 7 include "Arithmetic.ma".8 8 9 9 ninductive SFR8051: Type[0] ≝ … … 85 85 }. 86 86 87 alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)". 87 88 89 ndefinition set_8051_sfr ≝ 90 λs: Status. 91 λi: SFR8051. 92 λb: Byte. 93 let index ≝ sfr_8051_status i in 94 let 88 95 89 96 ndefinition initialise_status ≝ 90 mk_Status91 (Stub Byte sixteen)92 (Stub Byte seven)93 (Stub Byte seven)94 (Stub Bytesixteen)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. 
Deliverables/D4.1/Matita/Vector.ma
r256 r259 54 54 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 55 55 56 nlet rec set_index (A: Type[0]) (n: Nat) 57 (v: Vector A n) (m: Nat) (a: A) on m ≝ 56 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m ≝ 57 match m return (λx. x < n → A) with 58 [ Z ⇒ 59 match v with 60 [ Empty ⇒ λ_.? 61  Cons p hd tl ⇒ λ_.hd 62 ] 63  S o ⇒ 64 match v with 65 [ Empty ⇒ λ_.? 66  Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a 67 ] 68 ]. 69 70 nlet rec set_index_weak (A: Type[0]) (n: Nat) 71 (v: Vector A n) (m: Nat) (a: A) on m ≝ 58 72 match m with 59 73 [ Z ⇒ … … 66 80 [ Empty ⇒ Nothing (Vector A n) 67 81  Cons p hd tl ⇒ 68 let settail ≝ set_index A p tl o a in82 let settail ≝ set_index_weak A p tl o a in 69 83 match settail with 70 84 [ Nothing ⇒ Nothing (Vector A n)
Note: See TracChangeset
for help on using the changeset viewer.