ECS: Show example of using a Sum to delete a component

paulcadman · Sep 17, 2024 · a4da719 · a4da719
1 parent 7bab52f
commit a4da719
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/lean/Examples/BouncingBall.lean b/lean/Examples/BouncingBall.lean
@@ -79,6 +79,12 @@ def deleteAt' (pos : Vector2) (radius : Float) : Position × Entity → System W
     (← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
     then destroy (Position × Velocity) e else return ()
 
+/-- An alternative to `deleteAt` that uses a Sum to delete an entry --/
+def deleteAt'' (pos : Vector2) (radius : Float) : Position → System World (Unit ⊕ Not Position)
+  | ⟨p⟩ => do if
+    (← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
+    then return .inr .Not else return .inl ()
+
 def update : System World Unit := do
   let c : Config ← get global
   if (← isMouseButtonPressed MouseButton.left) then