RFC: `unless` doesn't support hypothesis like e.g. `if h: ...`

Proposal

A lot of (most?) control statements support a hypothesis on the condition they evaluate, however unless does not. It would be useful to add this, esp. in light of my other proposal/PR about extending the hypothesis scope: #5585.

This isn't just an attempt to make the language more "uniform" but has real practical implications on code correctness and potentially performance. Testing a condition and taking an early return is a very common operation and Lean should support writing the code as "naturally" as possible.

• User Experience
  (Especially in combination) The above two features would result in being able to write code like this:

def getFirst(arr : Array Nat) : Option Nat :=
   unless h: arr1.size > 0 return none
   return arr[0]   -- Note no []! index needed

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

This seems to be a fairly common pattern in the Lean source code e.g. in BrecOn.lean in replaceRecApps

                unless xs.size = numParams do
                  throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
                let belowForAlt := xs[numParams - 1]!       -- Note the []! here

or InlineCandidate.lean in inlineCandidate?:

      unless paramIdx < args.size do return none
      let arg := args[paramIdx]!

• Maintainability: Will this change streamline code maintenance or simplify its structure?

As demonstrated by the examples directly from the Lean's source.

Community Feedback

I have brought this up on Zulip previously and it has resurfaced here

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the existing hypothesis support for control statements and the examples in BrecOn.lean and InlineCandidate.lean. Compare the proposal with the related hypothesis-scope work in issue #5585 and the linked Zulip discussion. Done means unless h: ... works with the demonstrated early-return and indexing patterns, with suitable tests added.