From c3b239cc6f9b1a3742c90a8004144e07a5442fce Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 17 Sep 2024 15:38:02 +0100
Subject: [PATCH] ECS: Add Component instances for Unit

---
 lean/ECS/Basic.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/lean/ECS/Basic.lean b/lean/ECS/Basic.lean
index 6fb4c1a..82289d7 100644
--- a/lean/ECS/Basic.lean
+++ b/lean/ECS/Basic.lean
@@ -225,3 +225,28 @@ instance
       match mv with
         | none => ExplDestroy.explDestroy st ety
         | some x => ExplSet.explSet st ety x
+
+/-- Instances for Unit.
+Useful when you want to 'do nothing' in a cmap
+--/
+axiom ElemUnitStore : ElemFam Unit = Unit
+instance : FamilyDef ElemFam Unit Unit := ⟨ElemUnitStore⟩
+
+axiom StorageUnit : StorageFam Unit = Unit
+instance : FamilyDef StorageFam Unit Unit := ⟨StorageUnit⟩
+
+instance : @Component Unit Unit Unit _ _ where
+  constraint := rfl
+
+instance : @Has w Unit Unit _ where
+  getStore := return ()
+
+instance : @ExplGet Unit Unit _ where
+  explGet _ _ := return ()
+  explExists _ _ := return true
+
+instance : @ExplSet Unit Unit _ where
+  explSet _ _ _ := return ()
+
+instance : ExplDestroy Unit where
+  explDestroy _ _ := return ()