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

Last change on this file since 374 was 246, checked in by mulligan, 9 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.