From 20f41deea72d45bfb8236b44f27e8b11184b4467 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 1 Sep 2022 14:19:46 +0200
Subject: [PATCH] feat: add `Eval` instance for `BaseIO`

---
 src/Init/System/IO.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 2c8160cf46..7d7dc4e2af 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -697,6 +697,11 @@ instance [Eval α] : Eval (IO α) where
     let a ← x ()
     Eval.eval fun _ => a
 
+instance [Eval α] : Eval (BaseIO α) where
+  eval x _ := do
+    let a ← x ()
+    Eval.eval fun _ => a
+
 @[noinline, nospecialize] def runEval [Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit) :=
   IO.FS.withIsolatedStreams (Eval.eval a false |>.toBaseIO)