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  

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.