minor fix

lean-dojo · Feb 26, 2024 · f7c3791 · f7c3791
1 parent 4fa80e5
commit f7c3791
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/src/lean_dojo/interaction/Lean4Repl.lean b/src/lean_dojo/interaction/Lean4Repl.lean
@@ -4,6 +4,8 @@ import Lean.Elab.Frontend
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Command Lean.Elab.Tactic
 
+set_option autoImplicit false
+
 namespace LeanDojo
 
 
@@ -50,18 +52,18 @@ structure ReplState (σ : Type _) where
 
 
 /-- Get the saved tactic state with the given ID. --/
-private def getSavedState? (m : Type → Type) [Monad m] [MonadState (ReplState σ) m] (sid : Nat) : m (Option σ) := do
+private def getSavedState? (m : Type → Type) [Monad m] {σ : Type _} [MonadState (ReplState σ) m] (sid : Nat) : m (Option σ) := do
   return (← get).savedStates[sid]?
 
 
 /-- Get the initial tactic state. --/
-private def getInitialState! (m : Type → Type) [Monad m] [MonadState (ReplState σ) m] [MonadError m] : m σ := do
+private def getInitialState! (m : Type → Type) [Monad m] {σ : Type _} [MonadState (ReplState σ) m] [MonadError m] : m σ := do
   let some ts ← getSavedState? m 0 | throwError "[fatal] no initial state"
   return ts
 
 
 /-- Get the next state ID. --/
-private def getNextSid (m : Type → Type) [Monad m] [MonadState (ReplState σ) m] : m Nat := do
+private def getNextSid (m : Type → Type) [Monad m] {σ : Type _} [MonadState (ReplState σ) m] : m Nat := do
   return (← get).savedStates.size