Changeset 262 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 23, 2010, 4:39:31 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r261 r262 26 26 (* ===================================== *) 27 27 28 interpretation "Vector nil" 'nil = (Empty ?). 28 notation "[[ list0 x sep ; ]]" 29 non associative with precedence 90 30 for ${fold right @'vnil rec acc @{'vcons $x $acc}}. 31 32 interpretation "Vector vnil" 'vnil = (Empty ?). 33 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). 29 34 interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl). 30 31 notation "hvbox (v break !! n)"32 non associative with precedence 9033 for @{ 'get_index $v $n }.34 35 35 36 (* ===================================== *) … … 81 82 82 83 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 83 84 85 (* 84 86 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 ≝ 85 87 (match m with … … 98 100 nassumption. 99 101 nqed. 102 *) 100 103 101 104 nlet rec set_index_weak (A: Type[0]) (n: Nat) … … 224 227 ]. 225 228 226 notation "v break @ q"227 right associative with precedence 47228 for @{ 'append $v $q }.229 230 229 interpretation "Vector append" 'append hd tl = (append ? ? hd tl). 231 230
Note: See TracChangeset
for help on using the changeset viewer.