source: Deliverables/D4.1/Matita/Util.ma @ 229

Last change on this file since 229 was 229, checked in by mulligan, 10 years ago

More changes.

File size: 298 bytes
Line 
1include "logic/pts.ma".
2
3ndefinition function_apply ≝
4  λA, B: Type[0].
5  λf: A → B.
6  λa: A.
7    f a.
8   
9notation "f break $ x"
10  left associative with precedence 99
11  for @{ 'function_apply $f $x }.
12 
13interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
Note: See TracBrowser for help on using the repository browser.