From 332151dac0f38232074e1e386f31bb14651ed869 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Fri, 6 Sep 2024 00:12:26 +0100
Subject: [PATCH] Add comment to clarify where World and initWorld come from

---
 lean/Examples/BasicECS.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lean/Examples/BasicECS.lean b/lean/Examples/BasicECS.lean
index e21f7d5..ae540ee 100644
--- 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