JPYC.pure_eq

名称・種別

• 名称: JPYC.pure_eq
• 種別: theorem
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:37-38
• 概要: Except Error における pure は Except.ok である、という補題。
• 仕様: 対象外

型シグネチャ

∀ {β : Type} (a : β), Eq (Except.instMonad.pure a) (Except.ok a)

Except Error における pure a は Except.ok a に等しい、という定義的な等式です。

和訳 docstring

Except Error における pure は Except.ok。

解説

何を述べているか。 モナドの pure a（「何もせず値 a を返す」）が、Except においては成功 Except.ok a そのものだと明示します。

直感。 モデルの各関数は最後に pure (...) で結果を返します。それが Except.ok (...) だと分かれば、do ブロックの末尾を成功値として読み解けます。

なぜ安全性に効くか。 これも証明インフラです。checkAllowlist_bind_eq_ok などで、pure 枝を .ok として読み替えるために使います。状態を直接取り出す証明では、より高水準の補助 pure_ok を使います。

図解

Lean ソースコード

/-- `pure` in `Except Error` is `Except.ok`. -/
theorem pure_eq {β : Type} (a : β) : (pure a : Except Error β) = Except.ok a := rfl

依存

• JPYC.Error