| ;; |
| ;; General definitions |
| ;; |
| |
| ;; General variables |
| |
| syntax N hint(macro) = nat ;; hack |
| syntax M hint(macro) = nat ;; hack |
| syntax n hint(macro) = nat ;; hack |
| syntax m hint(macro) = nat ;; hack |
| |
| |
| ;; General constants |
| |
| def $Ki : nat |
| def $Ki = 1024 |
| |
| |
| ;; General functions |
| |
| def $min(nat, nat) : nat |
| def $min(i, j) = i -- if $(i <= j) |
| def $min(i, j) = j -- otherwise |
| |
| def $sum(nat*) : nat ;; TODO: hint |
| def $sum(eps) = 0 |
| def $sum(n n'*) = $(n + $sum(n'*)) |
| |
| |
| ;; General sequence functions |
| |
| def $opt_(syntax X, X*) : X? hint(show %2) |
| def $opt_(syntax X, eps) = eps |
| def $opt_(syntax X, w) = w |
| |
| def $list_(syntax X, X?) : X* hint(show %2) |
| def $list_(syntax X, eps) = eps |
| def $list_(syntax X, w) = w |
| |
| def $concat_(syntax X, (X*)*) : X* hint(show $concat(%2)) |
| def $concat_(syntax X, eps) = eps |
| def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*) |
