From c5f563598d1ad4c82ada1af890fd67e290b745b1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 6 Nov 2023 11:43:57 -0800
Subject: [PATCH] chore: Remove unnecessary unsafe's

---
 Main.lean      | 2 +-
 Test/Main.lean | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Main.lean b/Main.lean
index d7f936e..20caa1e 100644
--- a/Main.lean
+++ b/Main.lean
@@ -22,7 +22,7 @@ def parseCommand (s: String): Except String Protocol.Command := do
       return { cmd := s.take offset, payload := payload }
   | .none => throw "Command is empty"
 
-unsafe def loop : MainM Unit := do
+partial def loop : MainM Unit := do
   let state ← get
   let command ← (← IO.getStdin).getLine
   if command.trim.length = 0 then return ()
diff --git a/Test/Main.lean b/Test/Main.lean
index 5b9a24a..aee361c 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -6,8 +6,7 @@ import Test.Serial
 
 open Pantograph.Test
 
-unsafe def main := do
-  Lean.enableInitializersExecution
+def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [