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

1  include "Nat.ma". 

2  

3  ndefinition function_apply ≝ 

4  λA, B: Type[0]. 

5  λf: A → B. 

6  λa: A. 

7  f a. 

8  

9  notation "f break $ x" 

10  left associative with precedence 99 

11  for @{ 'function_apply $f $x }. 

12  

13  interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). 

14  

15  nlet 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.