include "Nat.ma".

ndefinition function_apply ≝
  λA, B: Type[0].
  λf: A → B.
  λa: A.
    f a.
    
notation "f break $ x"
  left associative with precedence 99
  for @{ 'function_apply $f $x }.
  
interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).

nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝
  match n with
    [ Z ⇒ a
    | S o ⇒ f (iterate A f a o)
    ].