| ;; |
| ;; Auxiliary definitions used for describing binary text notation |
| ;; |
| |
| ;; Text format |
| |
| ;; Defined in X.4-notation.binary |
| ;;syntax symdots hint(show `...) hint(macro none) = 0 |
| |
| ;;def $var(syntax X) : nat hint(show %) hint(macro none) |
| ;;def $var(syntax X) = 0x00 |
| |
| grammar Tvar(syntax X) : () hint(show %) hint(macro none) = 0x00 => () |
| grammar Tsym : A hint(macro none) = Tvar(T_1) => $var(A_1) | Tvar(symdots) | Tvar(T_n) => $var(A_n) |
| |
| grammar Tsymsplit/1 : () hint(show Tsym) hint(macro none) = Tvar(B_1) | ... |
| grammar Tsymsplit/2 : () hint(show Tsym) hint(macro none) = ... | Tvar(B_2) |
| |
| syntax abbreviated hint(macro none) = () |
| syntax expanded hint(macro none) = () |
| syntax `syntax hint(macro none) = () |
| |
| grammar Tabbrev : () hint(show Tsym) hint(macro none) = |
| Tvar(abbreviated) Tvar(syntax `syntax) == Tvar(expanded) Tvar(syntax `syntax) |
