summaryrefslogtreecommitdiff
path: root/tests/lean/Demo
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Demo')
-rw-r--r--tests/lean/Demo/Demo.lean1
1 files changed, 1 insertions, 0 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 48ac2062..2bbc385d 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -112,6 +112,7 @@ divergent def list_nth_mut1_loop
/- [demo::list_nth_mut1]:
Source: 'tests/src/demo.rs', lines 71:0-71:77 -/
+@[reducible]
def list_nth_mut1
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))