commit a2dd74df3c1f89e01d97074736007a2263186bb8
parent e1322d29a0296190d82aea0f26fabdb46fb06aba
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Wed, 24 Jul 2024 11:38:39 -0700
Switch to simpler way of creating NSpace vectors
Unfortunately, List.length is not reducible, so we have to do weird things in order to infer the correct instances.
Diffstat:
1 file changed, 7 insertions(+), 18 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -72,24 +72,13 @@ instance [Field F] [AddGroup V] [VectorSpace F V] : VectorSpace F (FunctionSpace
abbrev NSpace (n : Nat) (V : Type) := FunctionSpace (Fin n) V
instance [ToString V] : ToString (NSpace n V) where
toString f :=
- let coordStr i acc := toString (f i) :: acc
- s!"({String.intercalate ", " $ Fin.foldr n coordStr []})"
+ let coordToString i acc := toString (f i) :: acc
+ s!"({String.intercalate ", " $ Fin.foldr n coordToString []})"
-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 vec (coords : List V) : NSpace coords.length V := coords.get
def main : IO Unit :=
- IO.println $ (2 : Rat) ⋅ vec 4 1 0 0 9 + vec 4 0 1 0 1
+ let u : NSpace 2 Rat := vec [1, 0]
+ let v : NSpace 2 Rat := vec [0, 1]
+ let w := u + v
+ IO.println w
