how to do matrix vector multiplication with \b+ notation?

[alok]

I want to emulate the einsum op r c, c -> r with the box notation.

[lecopivo]

I do not understand what r c, c -> r is supposed to mean.

You can define matrix multiplication as

def matMul {n m : Nat} (A : Float^[n,m]) (x : Float^[m]) :=
  ⊞ i => ∑ j, A[i,j] * x[j]

[lecopivo]

I fixed the problem with Id' which was causing issues all over. Now you can do

import SciLean

open SciLean

variable {I J} [IndexType I] [IndexType J] [RealScalar R] [PlainDataType R]

instance : HMul (R^[I,J]) (R^[J]) (R^[I]) :=
  ⟨fun A x => ⊞ i => ∑ j, A[i,j] * x[j]⟩

def A := ⊞[1.0,2.0;0.0,3.0]
def x := ⊞[1.0,1000]

#eval A * x -- ⊞[2001.000000, 3000.000000]

Unfortunately this is broken

#eval ⊞[1.0,2.0;0.0,3.0] * ⊞[1.0,1000]

there is probably some incorrect elaboration order.

[alok]

Ascribing fixes the last one but ofc ascribing is annoying: #eval (⊞[1.0,2.0; 0.0,3.0]: Float^[2,2]) * (⊞[1,1000]: Float^[2])