Help in Heapify

Stream: new members

[Debangan Mishra]

Hello, I am trying to implement recursive heapification of an array in lean, but I am unable to perform the recursion. Could you please help me with correcting and improving my code?

import data.list.basic
import data.list

def convert_to_nat (value : option ℕ  ) : ℕ :=
  match value with
  | none := 0
  | some n := n
  end

def heapify (arr : list ℕ) (i : ℕ) : list ℕ  :=
  let largest : ℕ := i,
      l : ℕ := 2 * i + 1,
      r : ℕ := 2 * i + 2,
      leftval:= convert_to_nat (arr.nth l),
      rightval:= convert_to_nat (arr.nth r),
      maxval:= convert_to_nat (arr.nth largest),
      len:= arr.length
  in
  if (l < len) ∧ (leftval > maxval) then
    let largest := l,
        nmax := convert_to_nat (arr.nth largest)
      in
      if largest ≠ i then
        let list2 := arr.update_nth i (nmax),
            list3 := list2.update_nth largest (maxval)
        in
          heapify arr len largest
      else
        arr
  else
    if (r < len) ∧ (rightval > maxval) then
      let largest := r,
        nmax := convert_to_nat (arr.nth largest)
      in
      if largest ≠ i then
        let list2 := arr.update_nth i (nmax),
            list3 := list2.update_nth largest (maxval)
        in
          heapify arr len largest
      else
        arr
    else
      arr

[Kevin Buzzard]

Is this Lean 3? Do you have any reason not to upgrade to Lean 4? Lean 3 and mathlib3 are now retired.