chore: modify MonadStats to not extend parents multiple times (#169)

leanprover-community · Oct 22, 2024 · 9ac1294 · 9ac1294
1 parent b20a886
commit 9ac1294
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Aesop/Stats/Basic.lean b/Aesop/Stats/Basic.lean
@@ -175,12 +175,12 @@ end Stats
 
 abbrev StatsRef := IO.Ref Stats
 
-class MonadStats (m) extends
- MonadLiftT (ST IO.RealWorld) m,
- MonadLiftT BaseIO m,
- MonadOptions m where
+class MonadStats (m) extends MonadOptions m where
+ [instLift : MonadLiftT BaseIO m]
  readStatsRef : m StatsRef
 
+instance [MonadStats m] : MonadLift BaseIO m := ⟨MonadStats.instLift.monadLift⟩
+
 export MonadStats (readStatsRef)
 
 variable [Monad m]