Change variable value inside type

Stream: new members

[Vivek Rajesh Joshi]

What do I do here to tell Lean that RowEchelonForm.nil is of the right type?

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable (F : Type) [Field F] [DecidableEq F]

inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m n.succ
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm m n.succ

def Matrix.toRowEchelonForm (M : Matrix (Fin m) (Fin n) F) (i : Fin m) (j : Fin n) : RowEchelonForm F m n :=
  if n=0 then RowEchelonForm.nil (F:=F) (m:=m)                        --error
  else sorry

Error:

application type mismatch
  ite (n = 0) RowEchelonForm.nil
argument
  RowEchelonForm.nil
has type
  RowEchelonForm F m 0 : Type
but is expected to have type
  RowEchelonForm F m n : Type

[Vivek Rajesh Joshi]

Never mind, got it. match n with ... does the job.

[louq]

(deleted)