From f9f3b806a283ef651063a9bc976460f80a14580a Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Tue, 24 Oct 2023 17:12:52 +0200 Subject: [PATCH] Add warmup.v to _CoqProject --- _CoqProject | 2 +- theories/type_systems/warmup/warmup.v | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/_CoqProject b/_CoqProject index 506368d..6c39e65 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/type_systems/warmup/warmup.v b/theories/type_systems/warmup/warmup.v index 12055dc..5b2ac27 100644 --- a/theories/type_systems/warmup/warmup.v +++ b/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 *)