diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index a6a4e82a..0fb276aa 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -421,6 +421,19 @@ namespace Test progress simp [*] + /- Checking that progress can handle nested blocks -/ + example {α : Type} (v: Vec α) (i: Usize) (x : α) + (hbounds : i.val < v.length) : + ∃ nv, + (do + (do + let _ ← v.update_usize i x + .ret ()) + .ret ()) = ret nv + := by + progress + simp [*] + end Test end Progress |