Changeset 266
 Timestamp:
 Nov 23, 2010, 5:10:40 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r263 r266 33 33 λb: BitVector n. 34 34 λm: Nat. 35 get_index Bool n b m. 35 λp: m < n. 36 get_index Bool n b m p. 36 37 37 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). … … 41 42 λb: BitVector n. 42 43 λm: Nat. 43 set_index_weak Bool n b m. 44 λp: m < n. 45 λc: Bool. 46 set_index_weak Bool n b m c. 44 47 45 48 ndefinition drop ≝ 
Deliverables/D4.1/Matita/Interpret.ma
r265 r266 221 221 λs: Status. 222 222 let sfr ≝ special_function_registers_8051 s in 223 let psw ≝ get_index … ( get_8051_index SFR_PSW) s ? in223 let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in 224 224 get_index … Z psw ?. 225 225 
Deliverables/D4.1/Matita/Vector.ma
r265 r266 83 83 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 84 84 85 (*86 85 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝ 87 86 (match m with … … 100 99 nassumption. 101 100 nqed. 102 *)103 101 104 102 nlet rec set_index_weak (A: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.