diff options
| author | Aymeric Fromherz | 2024-05-23 16:46:18 +0200 |
|---|---|---|
| committer | Aymeric Fromherz | 2024-05-23 16:46:18 +0200 |
| commit | 765cb792916c1c69f864a6cf59a49c504ad603a2 (patch) | |
| tree | 66833e6ec5981ad4c2e1a0c836ffde4fef7ed9c9 /tests/lean/BetreeMain | |
| parent | e76ef95ddda11d4220e1f0fd863b0df568de95bc (diff) | |
Regenerate Lean files for betree
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/BetreeMain/Types.lean | 4 |
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 |