Idiomatic way to error out if a value is not none

Stream: new members

[Vlad Tsyrklevich]

I want to verify that a function returns none in some meta-code, I am currently doing

  let none := (← get).env.constants.find? name | elabTheorem stx

which seems better than

  if (← get).env.constants.contains name then
    elabTheorem stx
    return

but let none := seems a bit odd to me, is there a more idiomatic way to do this?

[Aaron Liu]

Maybe docs#guard with docs#Option.isNone

[Eric Wieser]

if let some existing := ... then return ... is another option