diff options
author | Son HO | 2024-01-27 21:51:38 +0100 |
---|---|---|
committer | GitHub | 2024-01-27 21:51:38 +0100 |
commit | 689954a5c84c29c9b86f02e5009f286d909c355c (patch) | |
tree | 0e801b5e01eda423d49bdb0a43cff11d65e78bb1 /backends/lean/Base/Primitives/Base.lean | |
parent | 202f0153dc51983e6bc0eddb65d22c763579850c (diff) | |
parent | d8247d99520738188bbd160be7de03550f8156ce (diff) |
Merge pull request #66 from AeneasVerif/son/lean
Improve the Lean backend
Diffstat (limited to 'backends/lean/Base/Primitives/Base.lean')
-rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 3d70c84a..9dbaf133 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -116,6 +116,13 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := @[simp] theorem bind_tc_div (f : α → Result β) : (do let y ← div; f y) = div := by simp [Bind.bind, bind] +@[simp] theorem bind_assoc_eq {a b c : Type u} + (e : Result a) (g : a → Result b) (h : b → Result c) : + (Bind.bind (Bind.bind e g) h) = + (Bind.bind e (λ x => Bind.bind (g x) h)) := by + simp [Bind.bind] + cases e <;> simp + ---------- -- MISC -- ---------- |