|
Last change
on this file since 265 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
|
| Rev | Line | |
|---|
| [243] | 1 | include "Nat.ma". |
|---|
| 2 | |
|---|
| [229] | 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 | |
|---|
| [243] | 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.
