Add warmup.v to _CoqProject

_CoqProject

@@ -13,4 +13,4 @@ theories/lib/maps.v
 theories/lib/sets.v
 
 # By removing the # below, you can add the exercise sheets to make
-#theories/type_systems/warmup/warmup.v
+theories/type_systems/warmup/warmup.v

theories/type_systems/warmup/warmup.v

@@ -25,7 +25,7 @@ Fixpoint expr_eval (e : expr) : Z :=
     | Mul a b => (expr_eval a) * (expr_eval b)
   end.
 
-Check expr_eval (Mul (Const 3) (Const 2)).
+(* Check expr_eval (Mul (Const 3) (Const 2)). *)
 
 (** Now let's define some notation to make it look nice! *)
 (* We declare a so-called notation scope, so that we can still use the nice notations for addition on natural numbers [nat] and integers [Z]. *)
@@ -38,10 +38,10 @@ Notation "e1 * e2" := (Mul e1%Z e2%Z) : expr.
     (note the [%E] to tell Coq to parse this as an arithmetical expression with the
     notations we just defined).
   *)
- Check (Const 5 + Const 5)%E.
+ (* Check (Const 5 + Const 5)%E. *)
  (* The notation also still works for [Z] and [nat]: *)
- Check (5 + 5)%Z.
- Check (5 + 5).
+ (* Check (5 + 5)%Z. *)
+ (* Check (5 + 5). *)
 
  (* As an exercise, rephrase the following lemmas using the newly defined notation *)