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

Last change on this file since 287 was 246, checked in by mulligan, 10 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

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.