feat: `x[i,j,k]` and `x[i,j,k] := xi` notation for Indexed

[lecopivo]

Get and set element notation for Indexed type. It should fall back to Lean's element notation using GetElem class if the there is not Indexed instance on the type.

Unexpander for get is also included.

Notation for slices using ranges is included but elaboration is not implemented.

Test file showcasing possibilities:

import LeanColls.Classes.Indexed.Notation

open LeanColls

def NDArray (α : Type) (ι : Type) [IndexType ι] := {a : Array α // a.size = IndexType.card ι}

instance {ι} [IndexType ι] : Indexed (NDArray α ι) ι α where
  mem := sorry
  toMultiset := sorry
  toMultiBagWithIdx := sorry
  fold := sorry
  ofFn := sorry
  get := sorry
  update := sorry

variable (x : NDArray Nat (Fin 10)) (t : NDArray Nat (Fin 10 × Fin 20 × Fin 20))

#check x[1]  -- x[1]

#check t[(1,2,3)] -- x[1,2,3]  -- yes it does not print back t[(1,2,3)]
#check t[1,(2,3)] -- x[1,2,3]  -- yes it does not print back t[1,(2,3)]
#check t[1,2,3]   -- x[1,2,3]

#check_failure t[1,:2,3:4] -- ranges are not yet supported - but syntax is registered

#check show Id Unit from do

  let mut a : NDArray Nat (Fin 10 × Fin 20) := sorry

  for i in IndexType.univ (Fin 10) do
    for j in IndexType.univ (Fin 20) do
      a[i,j] ← (pure 10)
      a[i,j] := 42
      a[i,j] += 42
      a[i,j] -= 42
      a[i,j] *= 42
      a[i,j] /= 42
      a[i,j] •= 42

-- check we didn't mess up Lean's indexing
variable (a : Array Nat) (i j : Fin a.size)

#check a[i]
#check a[:i]
#check a[i:]
#check a[i:j]