From 976646fb67f3c86365b06ac1e5332047444ea3aa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:11:05 -0800 Subject: [PATCH] chore: Use repeat-break structure --- Main.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Main.lean b/Main.lean index be01ff6..b20724d 100644 --- a/Main.lean +++ b/Main.lean @@ -23,10 +23,10 @@ def parseCommand (s: String): Except String Command := do return { cmd := s.take offset, payload := payload } | .none => throw "Command is empty" -partial def loop : MainM Unit := do +partial def loop : MainM Unit := do repeat do let state ← get let command ← (← IO.getStdin).getLine - if command.trim.length = 0 then return () + if command.trim.length = 0 then break match parseCommand command with | .error error => let error := Lean.toJson ({ error := "command", desc := error }: InteractionError) @@ -43,7 +43,6 @@ partial def loop : MainM Unit := do let message ← e.toMessageData.toString let error := Lean.toJson ({ error := "main", desc := message }: InteractionError) IO.println error.compress - loop unsafe def main (args: List String): IO Unit := do