fix: also check existance of first world of a Dependency arrow #292

leanprover-community · Feb 25, 2025 · 368b154 · 368b154
1 parent 28da6ea
commit 368b154
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/server/GameServer/Command/Dependency.lean b/server/GameServer/Command/Dependency.lean
@@ -23,6 +23,9 @@ elab "Dependency" s:Parser.dependency : command => do
     let some source := source?
       | do
           source? := some stx.getId
+          match (← getCurGame).worlds.nodes.get? stx.getId with
+          | some _ => pure ()
+          | none => logErrorAt stx m!"World `{stx.getId}` seems not to exist"
           continue
     let target := stx.getId
     match (← getCurGame).worlds.nodes.get? target with