Add comment to clarify where World and initWorld come from

paulcadman · Sep 5, 2024 · 332151d · 332151d
1 parent 8ffd62f
commit 332151d
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/lean/Examples/BasicECS.lean b/lean/Examples/BasicECS.lean
@@ -10,6 +10,7 @@ namespace BasicECS
 structure Camera where
   camera : Camera3D
 
+-- Brings `World` and `initWorld` into scope
 makeWorldAndComponents Camera
 
 def init : System World Unit := do