dependent `guard` syntax?

Stream: lean4

[Asei Inoue]

While it is convenient to use the guard function within a monadic context, how can we assign names to the propositions being guarded, as in the following example?

def bar (x : Nat) (_ : x % 2 == 0) := x

def foo (i : Nat) (arr : Array Nat) : Option Nat := do
  let x ← arr.get? i
  if h : x % 2 == 0 then
    some (bar x h)
  else
    none

[Eric Wieser]

I found myself needing this the other day, and used

let ⟨h⟩ <- if h : P then PLift.up h else failure

[Eric Wieser]

(in my case I actually used throwError not failure)

[Eric Wieser]

Ideally we'd have unless h : P do failure as syntax for this

[Edward van de Meent]

i seem to recall someone working on this/something along these lines?

[Edward van de Meent]

i feel like there might be a lean issue/pr for it

[Edward van de Meent]

unfortunately, i can't find it

[Joachim Breitner]

Do you mean https://github.com/leanprover/lean4/issues/5598?

[Edward van de Meent]

that might be it, although i also remember this involving if without else... that might just be wishful thinking on my part though :upside_down:

[Damiano Testa]

Edward, maybe you were thinking of this or this?

[Edward van de Meent]

yes, that second one is it!

[Eric Wieser]

I put a snippet you can copy/paste on lean4#5598