Naming condition (Prop) in while notation

Stream: lean4

[Andrés Goens]

I'm trying to use the new a[i]'h notation for array access in an (unapologetically imperative) while loop, but I can't name the hypothesis. An MWE:

partial def foo' : Array Int → Int
  | arr => Id.run do
    let mut r : Int := 1
    -- while h : arr.size > 0 do
    while arr.size > 0 do
      r := r * arr[arr.size - 1]!
    return r

I can work-around this by using if, e.g.:

theorem n_minus_one_le_n {n : Nat} : n > 0 → n - 1 < n := by
  cases n with
  | zero => simp []
  | succ n =>
  intros
  rw [Nat.succ_eq_add_one, Nat.add_sub_cancel]
  apply Nat.le.refl

partial def foo : Array Int → Int
  | arr => Id.run do
    let mut r : Int := 1
    let mut cond : Bool := false
    while cond == false do
      if h : arr.size > 0 then
        r := r * arr[arr.size - 1]'(by apply n_minus_one_le_n h)
      else
        cond := true
    return r

but that's kind of a hack. Is there a fundamental reason why this hypothesis-naming syntax does not work in while? It's hard to figure out where that syntax is defined for if (is it even defined in the Lean part of the code?)?

[Leonardo de Moura]

https://github.com/leanprover/lean4/issues/1337