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


From cf7cd476b32cd562ca90950e4b3c29c9fc42028a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:25:17 +0200
Subject: Regenerate the tests

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

(limited to 'tests/lean/Demo')

diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 2bbc385d..a557cf73 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -2,6 +2,9 @@
 -- [demo]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace demo
 
-- 
cgit v1.2.3