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 | |
| Line | |
|---|---|
| 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.
