From c8c85195d7c930570e592e3836359b1da40d392b Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 9 Mar 2023 19:00:19 +0100
Subject: [PATCH] Branch

---
 server/leanserver/GameServer/Commands.lean               | 9 +++++++++
 .../testgame/TestGame/Levels/Function/L11_Inverse.lean   | 3 +++
 2 files changed, 12 insertions(+)

diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 27bc57f..cc2263a 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -102,6 +102,15 @@ elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
       .nest (if hidden then 1 else 0) $
       .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
 
+/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
+proof state. We use it to define Hints for alternative proof methods or dead ends. -/
+elab "Branch" t:tacticSeq : tactic => do
+  let b ← saveState
+  Tactic.evalTactic t
+  let msgs ← Core.getMessageLog
+  b.restore
+  Core.setMessageLog msgs
+
 /-- Define the statement of the current level.
 
 Arguments:
diff --git a/server/testgame/TestGame/Levels/Function/L11_Inverse.lean b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean
index f7f34a8..5ee50f3 100644
--- a/server/testgame/TestGame/Levels/Function/L11_Inverse.lean
+++ b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean
@@ -21,6 +21,9 @@ open Function
 
 Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
     Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+  Branch
+    exfalso
+    Hint "Das war eine blöde Idee"
   Hint (hidden := true) "constructor"
   constructor
   Hint "intro h" -- does not show