Add subtraction to nexp grammar (removing the need to do a + (-1 * b))

Fix up parsing on 2** precedence
Fix errors on type variables in function definition

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