From 77f309cec8e2f119272640083bc3476e4121952c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Aug 2023 17:50:16 +0200
Subject: Regenerate the test files

---
 tests/lean/NoNestedBorrows.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/lean/NoNestedBorrows.lean')

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1a180c60..884e62c4 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -251,16 +251,16 @@ def test_char : Result Char :=
 
 mutual
 
-/- [no_nested_borrows::NodeElem] -/
-inductive NodeElem (T : Type) :=
-| Cons : Tree T → NodeElem T → NodeElem T
-| Nil : NodeElem T
-
 /- [no_nested_borrows::Tree] -/
 inductive Tree (T : Type) :=
 | Leaf : T → Tree T
 | Node : T → NodeElem T → Tree T → Tree T
 
+/- [no_nested_borrows::NodeElem] -/
+inductive NodeElem (T : Type) :=
+| Cons : Tree T → NodeElem T → NodeElem T
+| Nil : NodeElem T
+
 end
 
 /- [no_nested_borrows::list_length]: forward function -/
-- 
cgit v1.2.3