From 02978a38ed97545a54f5f3950657d55874d0d666 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 18 Apr 2024 18:22:03 +0200
Subject: [PATCH] add allowed keywords #215

---
 server/GameServer/EnvExtensions.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 20be5b3..d2a47d5 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -5,9 +5,14 @@ import GameServer.Hints
 open GameServer
 
 -- TODO: Is there a better place?
-/-- Keywords that the server should not consider as tactics. -/
+/-- Keywords that the server should not consider as tactics.
+
+Note: Added `clear` tactic because currently it is very useful in combination with
+`Branch` and `Hint` (i.e. using `clear` before a `Hint` in order to remove any irrelevant
+hypotheses).
+-/
 def GameServer.ALLOWED_KEYWORDS : List String :=
-  ["with", "fun", "at", "only", "by", "generalizing"]
+  ["with", "fun", "at", "only", "by", "generalizing", "if", "then", "else", "clear"]
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"