summaryrefslogtreecommitdiff
path: root/tests/lean/Demo/Demo.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Demo/Demo.lean')
-rw-r--r--tests/lean/Demo/Demo.lean4
1 files changed, 1 insertions, 3 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index f38b5cd3..09032820 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -116,9 +116,7 @@ def list_nth_mut1
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
:=
- do
- let (t, back_'a) ← list_nth_mut1_loop T l i
- Result.ret (t, back_'a)
+ list_nth_mut1_loop T l i
/- [demo::i32_id]:
Source: 'src/demo.rs', lines 80:0-80:28 -/