From 1021cdea98043dd935dbc8dbe633b90fda68047d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:15:26 +0200
Subject: Update the tests

---
 tests/lean/Demo/Demo.lean | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tests/lean/Demo')

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)))
-- 
cgit v1.2.3