Lean is far more punishing even for simple imperative code. The following is rejected: /- Return the array of forward differences between consecutive e

Lean is far more punishing even for simple imperative code. The following is rejected: /- Return the array of forward differences between consecutive elements of the input. Return the empty array if the input is empty or a singleton. -/ def diffs (numbers : Array Int) : Array Int := Id.run do if size_ok : numbers.size > 1 then let mut diffs := Array.mkEmpty (numbers.size - 1) for index_range : i in [0:numbers.size - 2] do diffs := diffs.push (numbers[i+1] - numbers[i]) return diffs else return #[]