Changeset 243 for Deliverables/D4.1
 Timestamp:
 Nov 15, 2010, 10:41:29 AM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Util.ma
r229 r243 1 1 include "logic/pts.ma". 2 3 include "Nat.ma". 2 4 3 5 ndefinition function_apply ≝ … … 12 14 13 15 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). 16 17 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝ 18 match n with 19 [ Z ⇒ a 20  S o ⇒ f (iterate A f a o) 21 ]. 
Deliverables/D4.1/Matita/Vector.ma
r241 r243 292 292 reverse A n (shift_left_1 A n (reverse A n v) a). 293 293 294 ncheck Nat. 295 294 296 ndefinition shift_left ≝ 295 297 λA: Type[0].
Note: See TracChangeset
for help on using the changeset viewer.