source: Deliverables/D4.1/Demo-March-2011/matita/Util.ma @ 644

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

Committed files for demo on Friday. Binary search works with O'Caml emulator. Need to check with submitted version of Matita emulator.

File size: 431 bytes
Line 
1include "Nat.ma".
2
3ndefinition function_apply ≝
4  λA, B: Type[0].
5  λf: A → B.
6  λa: A.
7    f a.
8   
9notation "f break $ x"
10  left associative with precedence 99
11  for @{ 'function_apply $f $x }.
12 
13interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
14
15nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝
16  match n with
17    [ Z ⇒ a
18    | S o ⇒ f (iterate A f a o)
19    ].
Note: See TracBrowser for help on using the repository browser.