summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/BetreeMain')
-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