Fix lean4 v4.14.0 deprecations

lean/ECS/Components.lean

@@ -100,7 +100,7 @@ It can also be used as:
 
 to delete every `a` component.
 --/
-inductive Not (α : Type) :=
+inductive Not (α : Type) where
   | Not
 
 

lean/Examples/BouncingBall.lean

@@ -20,7 +20,7 @@ structure Config where
   velocity : Vector2
   deriving Inhabited
 
-inductive Circle :=
+inductive Circle where
   | Circle
 
 -- Brings `World` and `initWorld` into scope

lean/Examples/JessicaCantSwim.lean

@@ -50,7 +50,7 @@ def main : IO Unit := do
     let keys ← getKeys
     let emits := game.emit
     let events: List Types.Msg := List.map (λ key => Types.Msg.Key key) keys
-    game := game.step delta (List.join [events, emits])
+    game := game.step delta (List.flatten [events, emits])
     let drawings := game.view
     let ⟨ ⟨ ox, oy ⟩, ⟨ tx, ty ⟩, r, z ⟩ := game.camera
     renderFrame do

lean/Examples/JessicaCantSwim/Game.lean

@@ -45,7 +45,7 @@ private def Game.update (game: Game) (msg: Types.Msg): Game :=
   }
 
 def Game.view (game: Game): List Draw.Draw :=
-  List.join [
+  List.flatten [
     -- Add your new Model here:
     game.wetsand.view,
     game.shells.view,
@@ -55,7 +55,7 @@ def Game.view (game: Game): List Draw.Draw :=
   ]
 
 def Game.emit (game: Game): List Types.Msg :=
-  List.join [
+  List.flatten [
     -- Add your new Model here:
     game.ocean.emit,
     game.wetsand.emit,