From a4da7194ded1fbfdf787a66e47d37e60388c24d1 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 17 Sep 2024 18:32:44 +0100 Subject: [PATCH] ECS: Show example of using a Sum to delete a component --- lean/Examples/BouncingBall.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/lean/Examples/BouncingBall.lean b/lean/Examples/BouncingBall.lean index 3b85a1a..bb1c266 100644 --- 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