Branch

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:

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