pattern for multiple guards before error?

Stream: lean4

[Thomas Murrills]

In MetaM (well, TacticM) I want to write something like

try
  guard ... -- easy check
  guard ... -- harder check
  guard ... -- hardest check
  throwError "all checks passed :("
catch _ =>
  foo

but, of course, this doesn't work the way I naively expect it to, because throwError is an error and thus gets caught by the catch.

I can use a .internal exception, but that seems a bit hacky for what should be a "nice" procedure: try a bunch of things in order; if they fail, do one thing, if they succeed, do another. (A little worried about simply using && in if because I'm not sure it short-circuits at the elaboration stage.)

Any advice to write this cleanly?

[Mario Carneiro]

I use the try? function for this

[Mario Carneiro]

it internally catches the exception and presents the result as an Option

[Mario Carneiro]

also, && does short-circuit

[Thomas Murrills]

oh, cool. this is the function in Mathlib.Control.Basic? so here the pattern would be something like...

let .none := try?
  guard ...
  guard ...
  guard ...
| throwError "checks passed :("
foo

up to syntax?

[Thomas Murrills]

(unfortunately I think I'm upstream of that file unless I reorganize, which, wouldn't be the worst thing)

[Thomas Murrills]

(oh, I think I can use return in my particular case, I think, since I do in fact want to foo; return ())