From 970c16a0a4d808c4be86cc313ff1f4acb3ff0aca Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 24 Jan 2025 20:19:07 -0800
Subject: [PATCH] chore: Use `StateRefT` in `Repl.lean`

---
 Repl.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Repl.lean b/Repl.lean
index ddf3201..4c7adc3 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -12,7 +12,9 @@ structure State where
   goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+abbrev MainM := ReaderT Context $ StateRefT State Lean.CoreM
+/-- Fallible subroutine return type -/
+abbrev CR α := Except Protocol.InteractionError α
 
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
@@ -24,10 +26,6 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   return stateId
 
 
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
--- certain monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
-
 def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
   metaM.run'
 def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=