source:
Deliverables/D4.1/Matita/Util.ma
@
229
Last change on this file since 229 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.