Changeset 266 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 23, 2010, 5:10:40 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.