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

Updated Util.ma too.

File:
1 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    ].
Note: See TracChangeset for help on using the changeset viewer.