diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index d9b410cd..eb598113 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -50,8 +50,9 @@ type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) + | Nexp_neg of nexp (* For internal use *) and nexp = | Nexp_aux of nexp_aux * l |