From 9b93e3817dcfe7a7ab15c6fcf35b51287c5dd5a3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:24 +0200 Subject: [PATCH] Update RpcHandlers.lean --- server/GameServer/RpcHandlers.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index e81bce4..ce4e61c 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -231,7 +231,7 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo -- Answer: The last snap only copied the diags from the end of this snap let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray - -- Level is completed if there are no errrors or warnings + -- Level is completed if there are no errors or warnings let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)