Matrix.of help

Stream: new members

[Newell Jensen]

I am trying to define a matrix with a function but I have only been able to get it to work using an auxiliary function. How can I get this to work without needing the auxiliary function?

import Mathlib.Data.Matrix.Notation

-- Errors
def test1 (n : ℕ) : Matrix (Fin n) (Fin n) ℕ+ :=
  Matrix.of fun i j => if i == j then 1 else (if i == n - 1 ∨ j == n -1 then 2 else 3)

def testAux : (Fin n) → (Fin n) → ℕ+ :=
  fun i j => if i == j then 1 else (if i == n - 1 ∨ j == n -1 then 2 else 3)

-- No Errors
def test2 (n : ℕ) : Matrix (Fin n) (Fin n) ℕ+ :=
  Matrix.of testAux

[Eric Wieser]

Providing explicit types on i and j helps:

def test1 (n : ℕ) : Matrix (Fin n) (Fin n) ℕ+ :=
  Matrix.of fun i j : Fin n => if i == j then 1 else (if i == n - 1 ∨ j == n -1 then 2 else 3)

[Eric Wieser]

I think Lean gets confused because of is an Equiv not a function, so doesn't work thinks out automatically

[Newell Jensen]

Ah okay, yeah, thanks.

[Eric Wieser]

Adding a by exact works too:

def test1 (n : ℕ) : Matrix (Fin n) (Fin n) ℕ+ :=
  Matrix.of <| by exact fun i j => if i == j then 1 else (if i == n - 1 ∨ j == n -1 then 2 else 3)