source:
Deliverables/D4.1/Matita/Util.ma
@
231
| Last change on this file since 231 was 229, checked in by , 10 years ago | |
|---|---|
| File size: 298 bytes | |
| Rev | Line | |
|---|---|---|
| [229] | 1 | include "logic/pts.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). |
Note: See TracBrowser
for help on using the repository browser.
