turn defeq-hints on by default #45

server/GameServer/Commands.lean

@@ -524,7 +524,7 @@ see hints. The tactic does not affect the goal state.
 elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
   let mut strict := false
   let mut hidden := false
-  let mut defeq := false
+  let mut defeq := true
 
   -- remove spaces at the beginning of new lines
   let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do

server/GameServer/Hints.lean

@@ -20,7 +20,7 @@ structure GoalHintEntry where
   hidden : Bool := false
   /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
   strict : Bool := false
-  defeq : Bool := false
+  defeq : Bool := true
 
 instance : Repr GoalHintEntry := {
   reprPrec := fun a n => reprPrec a.text n