From f7c37917ae959216db321e05ec22fb642e76dc31 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Mon, 26 Feb 2024 09:01:02 -0800 Subject: [PATCH] minor fix --- src/lean_dojo/interaction/Lean4Repl.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lean_dojo/interaction/Lean4Repl.lean b/src/lean_dojo/interaction/Lean4Repl.lean index 570f15fa..9cda505c 100644 --- 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