source: Deliverables/D4.1/Matita/Util.ma @ 243

Last change on this file since 243 was 243, checked in by mulligan, 9 years ago

Updated Util.ma too.

File size: 456 bytes
Line 
1include "logic/pts.ma".
2
3include "Nat.ma".
4
5ndefinition function_apply ≝
6  λA, B: Type[0].
7  λf: A → B.
8  λa: A.
9    f a.
10   
11notation "f break $ x"
12  left associative with precedence 99
13  for @{ 'function_apply $f $x }.
14 
15interpretation "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 TracBrowser for help on using the repository browser.