JPYC.error_bind

名称・種別

• 名称: JPYC.error_bind
• 種別: theorem
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:33-35
• 概要: Except.error は bind を短絡する、という補題。
• 仕様: 対象外

型シグネチャ

∀ {α β : Type} (e : JPYC.Error) (f : α → Except JPYC.Error β), Eq (Except.instMonad.bind (Except.error e) f) (Except.error e)

Except.error e >>= f は Except.error e に等しい、という定義的な等式です。

和訳 docstring

Except.error は束縛を短絡させる（後続を実行しない）。

解説

何を述べているか。 いったん Except.error e になった計算は、後続 f を 無視 してそのまま Except.error e を返します。

直感。 「一度 revert したら、その先の処理は実行されない」という短絡（short-circuit）です。これも定義から rfl で従います。

なぜ安全性に効くか。 Except と revert モデル の核心 ―「失敗は伝播し、以降の状態変更は起きない」― を支えます。bind_eq_ok がこの補題を使い、「成功したならどのガードも失敗していない」と逆向きに推論します。

図解

Lean ソースコード

/-- `Except.error` short-circuits a bind. -/
theorem error_bind {α β : Type} (e : Error) (f : α → Except Error β) :
    ((Except.error e : Except Error α) >>= f) = Except.error e := rfl

依存

• JPYC.Error