From 478d15fbe8968115c08c4df8bd6a621b1b0b9f7e Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 3 Sep 2024 21:22:52 +0100 Subject: [PATCH] Fix Vector2 addition --- lean/Raylean/Math.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean index 4b4595f..d914da8 100644 --- 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)