Skip to content

Commit

Permalink
Fix Vector2 addition
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Sep 3, 2024
1 parent 918911e commit 478d15f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lean/Raylean/Math.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit 478d15f

Please sign in to comment.