From 765cb792916c1c69f864a6cf59a49c504ad603a2 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 16:46:18 +0200
Subject: Regenerate Lean files for betree

---
 tests/lean/BetreeMain/Types.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 3f115fe4..e79da43f 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -46,15 +46,19 @@ inductive betree.Node :=
 
 end
 
+@[simp, reducible]
 def betree.Internal.id (x : betree.Internal) :=
   match x with | betree.Internal.mk x1 _ _ _ => x1
 
+@[simp, reducible]
 def betree.Internal.pivot (x : betree.Internal) :=
   match x with | betree.Internal.mk _ x1 _ _ => x1
 
+@[simp, reducible]
 def betree.Internal.left (x : betree.Internal) :=
   match x with | betree.Internal.mk _ _ x1 _ => x1
 
+@[simp, reducible]
 def betree.Internal.right (x : betree.Internal) :=
   match x with | betree.Internal.mk _ _ _ x1 => x1
 
-- 
cgit v1.2.3