commit e1322d29a0296190d82aea0f26fabdb46fb06aba parent 6b735780b681ed96b9212b6966b376db6cbf3178 Author: Robert Russell <robertrussell.72001@gmail.com> Date: Tue, 23 Jul 2024 22:11:09 -0700 Add cool variadic vec builder function Diffstat:
| M | Main.lean | | | 21 | ++++++++++++++++----- |
1 file changed, 16 insertions(+), 5 deletions(-)
diff --git a/Main.lean b/Main.lean @@ -75,10 +75,21 @@ instance [ToString V] : ToString (NSpace n V) where let coordStr i acc := toString (f i) :: acc s!"({String.intercalate ", " $ Fin.foldr n coordStr []})" -def vec3 (x y z : Rat) : NSpace 3 Rat := fun -| 0 => x -| 1 => y -| 2 => z +abbrev VecNBuilder (n : Nat) (V : Type) (i : Nat) := + match i with + | 0 => NSpace n V + | j + 1 => V -> VecNBuilder n V j + +def vec (n : Nat) : VecNBuilder n Rat n := + let rec build (i : Nat) (f : NSpace (n - i) Rat) : VecNBuilder n Rat i := + match i with + | 0 => f + | j + 1 => fun v => + let g := fun (x : Fin (n - j)) => + if h : x.val < n - (j + 1) then f (x.castLT h) else v + build j g + let f : NSpace (n - n) Rat := fun x => nomatch Fin.cast (Nat.sub_self n) x + build n f def main : IO Unit := - IO.println $ vec3 1 0 0 + vec3 0 1 0 + IO.println $ (2 : Rat) ⋅ vec 4 1 0 0 9 + vec 4 0 1 0 1