Merge pull request #23 from paulcadman/fix-vector2-add

Fix Vector2 addition
funexists · Sep 3, 2024 · 03543f7 · 03543f7
2 parents 918911e + 478d15f
commit 03543f7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean
@@ -9,7 +9,7 @@ namespace Vector2
 open Raylean.Types
 
 def add (v1 : Vector2) (v2 : Vector2) : Vector2 :=
-  { x := v1.x + v2.x, y := v1.y + v1.y : Vector2 }
+  { x := v1.x + v2.x, y := v1.y + v2.y : Vector2 }
 
 def length (v : Vector2) : Float := Float.sqrt (v.x ^ 2 + v.y ^ 2)