Allow negative numbers in expressions

lean/Spa/Language/Semantics.lean

@@ -33,7 +33,7 @@ inductive Env.Mem : String × Value → Env → Prop
 /-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
     environment. Pretty standard big-step expression evaluation. -/
 inductive EvalExpr : Env → Expr → Value → Prop
-  | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
+  | num (ρ : Env) (z : ℤ) : EvalExpr ρ (.num z) (.int z)
   | var (ρ : Env) (x : String) (v : Value) :
       Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v
   | add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :