Changeset 243


Ignore:
Timestamp:
Nov 15, 2010, 10:41:29 AM (9 years ago)
Author:
mulligan
Message:

Updated Util.ma too.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Util.ma

    r229 r243  
    11include "logic/pts.ma".
     2
     3include "Nat.ma".
    24
    35ndefinition function_apply ≝
     
    1214 
    1315interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
     16
     17nlet 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  
    292292    reverse A n (shift_left_1 A n (reverse A n v) a).
    293293   
     294ncheck Nat.
     295   
    294296ndefinition shift_left ≝
    295297  λA: Type[0].
Note: See TracChangeset for help on using the changeset viewer.