summaryrefslogtreecommitdiff
path: root/tests/lean/Demo/Demo.lean
diff options
context:
space:
mode:
authorSon Ho2024-06-17 07:15:26 +0200
committerSon Ho2024-06-17 07:15:26 +0200
commit1021cdea98043dd935dbc8dbe633b90fda68047d (patch)
treedc2f420cf5167690da9dfebe358ba56bf05e1b1e /tests/lean/Demo/Demo.lean
parentf4739fba4be95818ca01776837c8d610e443a45b (diff)
Update the tests
Diffstat (limited to 'tests/lean/Demo/Demo.lean')
-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)))