From cd3363a62ea5d7db047a309ecac9b2775790766b Mon Sep 17 00:00:00 2001
From: JKTKops <zerglingk9012@gmail.com>
Date: Thu, 19 Aug 2021 14:09:01 -0500
Subject: [PATCH] Turn claim 3 of simple-spec into an exercise

---
 tests/control-flow/simple-spec.k | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/tests/control-flow/simple-spec.k b/tests/control-flow/simple-spec.k
index 281e6d7..500b3b1 100644
--- a/tests/control-flow/simple-spec.k
+++ b/tests/control-flow/simple-spec.k
@@ -16,8 +16,14 @@ module VERIFICATION
     imports SIMPLE-SPEC-SYNTAX
     imports CONTROL-FLOW
 
-    rule maxInt(X, Y) => Y requires         X <Int Y [simplification]
-    rule maxInt(X, Y) => X requires notBool X <Int Y [simplification]
+    // Leave these lemmas out to turn the third claim into an exercise;
+    // Make a note that lemmas are missing and that they go here. Exercise is to
+    // figure out that `maxInt` is missing lemmas and implementing them correctly should
+    // be easy.
+    // An easier exercise could leave off only one of these lemmas.
+    
+    // rule maxInt(X, Y) => Y requires         X <Int Y [simplification]
+    // rule maxInt(X, Y) => X requires notBool X <Int Y [simplification]
 endmodule
 
 module SIMPLE-SPEC