summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-23 16:46:18 +0200
committerAymeric Fromherz2024-05-23 16:46:18 +0200
commit765cb792916c1c69f864a6cf59a49c504ad603a2 (patch)
tree66833e6ec5981ad4c2e1a0c836ffde4fef7ed9c9
parente76ef95ddda11d4220e1f0fd863b0df568de95bc (diff)
Regenerate Lean files for betree
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Types.lean4
1 files changed, 4 insertions, 0 deletions
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