source: Deliverables/D4.1/DemoFinal/matita/Util.ma @ 3174

Last change on this file since 3174 was 671, checked in by mulligan, 10 years ago

Finished demo script for tomorrow.

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.