Branching on matched success/failure in monads

Stream: lean4

[Thomas Murrills]

What's the cleanest way to check if an operation succeeded and branch on the result while matching the original result? For example, if I have a (pre-existing) function which can fail, e.g. synthInstance, can I, in some other MetaM do block, write some variant of

if let i ← synthInstance e then ... else ...

(which doesn't seem to work as-is); or (in general) do I need to do something like

def synthInstance? (e : Expr) : MetaM (Option Expr) :=
return (some <|← synthInstance e) <|> none

(which I'm not totally sure does what I want it to in the first place) and then write if let some i ← synthInstance? e then ... else...? Is there a better way?

[Gabriel Ebner]

if let .. does pattern matching. You can do if let .some inst ← trySynthInstance ... then ... else ...

[Thomas Murrills]

Ok, gotcha, thanks! Good to know it's got to be pattern matching. :)