/usr/share/hol88-2.02.19940316/Library/latex-hol/precedence.ml is in hol88-library-source 2.02.19940316-19.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 | % precedence.ml %
%-----------------------------------------------------------------------------%
% Precedence tables for HOL %
% Values have been chosen to allow user-defined objects to have a %
% precedence between the precedences of any built-in objects. %
let is_res_quan =
(\con. mem con [`RES_FORALL`; `RES_EXISTS`; `RES_SELECT`; `RES_ABSTRACT`]);;
% Precedence table for HOL types %
let type_prec symb =
% : (string -> int) %
case symb
of `fun` . 300
| `prod` . 100
| `sum` . 200
| _ . 0;;
% Highest type precedence (minimum value) %
let min_type_prec = 0;;
% Lowest type precedence (maximum value) %
let max_type_prec = 400;;
% Precedence table for HOL terms %
let term_prec symb =
% : (string -> int) %
case symb
of `\\` . 1700 % Abstractions %
| `o` . 1600
| `Sum` . 1600
| `IS_ASSUMPTION_OF` . 1600
| `=` . 1500
| `<=>` . 1400
| `==>` . 1300
| `\\/` . 1200
| `/\\` . 1100
| `<` . 1000
| `>` . 1000
| `<=` . 1000
| `>=` . 1000
| `+` . 900
| `-` . 900
| `*` . 800
| `DIV` . 800
| `MOD` . 800
| `EXP` . 700
| `LET` . 600
| `COND` . 500
| `,` . 400 % Tuples %
| `~` . 300
| `:` . 100 % Type information %
| x . (if (is_binder x) then 1700
else if (is_res_quan x) then 1700
else if (is_infix x) then 200
else 0);;
% Highest term precedence (minimum value) %
let min_term_prec = 0;;
% Lowest term precedence (maximum value) %
let max_term_prec = 1800;;
%-----------------------------------------------------------------------------%
|