def Iris.ProofMode.try? {m : Type u_1 → Type u_2} {ε : Type u_3} {α : Type u_1} [Monad m] [MonadExcept ε m] (x : m α) : m (Option α)

Equations

• Iris.ProofMode.try? x = tryCatch (do let __do_lift ← x pure (some __do_lift)) fun (x : ε) => pure none