Pr/splaytree refactor 20260505#2
Merged
AntoineduFresne merged 8 commits intoMay 5, 2026
Merged
Conversation
…ree preservation, BST root preservation)\n\nCo-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Updated phi_zig theorem to use BinaryTree α and Frame α type parameters - Restored linarith proof for L.empty case - Note: Type parameter refactoring exposed some issues with split cases that need further investigation Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
nnhjy
added a commit
that referenced
this pull request
May 13, 2026
commit 2254a42 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 11:36:24 2026 +0200 update website commit c6b6be6 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 11:07:46 2026 +0200 remove theorem in blueprint commit 545d9fe Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 10:58:03 2026 +0200 blueprint commit 43350fd Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 10:51:41 2026 +0200 push commit 7bc2dd4 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 10:29:26 2026 +0200 Websites and workflows commit 99bb4b8 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Wed May 13 00:17:21 2026 +0200 Add GitHub Actions workflow for GitHub Pages deployment This workflow automates the deployment of static content to GitHub Pages upon pushes to the main branch or manual triggers. commit 3bef94e Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Tue May 12 23:46:15 2026 +0200 Add GitHub Actions workflow for Jekyll deployment This workflow automates the build and deployment of a Jekyll site to GitHub Pages, including steps for checking out the code, building the site, and uploading the artifact. commit 79dbf63 Merge: a393448 2a84ec9 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Tue May 12 23:38:26 2026 +0200 Merge pull request #6 from sorrachai:refactoring chore: add CI/CD workflow and github documentation page commit 2a84ec9 Author: Basil Rohner <basil.rohner@outlook.de> Date: Tue May 12 14:25:38 2026 +0200 add pr and pages workflow and page commit a393448 Merge: e75e46b 73b6bd7 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Tue May 12 11:55:31 2026 +0200 Merge pull request #5 from sorrachai:refactoring chore: refactoring into a clean library skeleton commit 73b6bd7 Author: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com> Date: Tue May 12 11:54:40 2026 +0200 Add data structure folder commit e1cbad5 Author: Basil Rohner <basil.rohner@outlook.de> Date: Tue May 12 09:50:03 2026 +0200 update readme commit 50fee8b Author: Basil Rohner <basil.rohner@outlook.de> Date: Mon May 11 23:08:20 2026 +0200 fixes commit 9a1f252 Author: Basil Rohner <basil.rohner@outlook.de> Date: Mon May 11 22:54:27 2026 +0200 refactoring commit e75e46b Author: AntoineduFresne <antoine@du-fresne.ch> Date: Thu May 7 17:14:43 2026 +0200 update + Optimisation of SplayTree.lean commit ae17b87 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Thu May 7 16:41:52 2026 +0200 The main amortized complexity of Splay tree commit 37dbe35 Merge: f4d7bbb 6150be5 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Tue May 5 11:41:46 2026 +0200 Merge upstream/main into main commit f4d7bbb Merge: 6485058 f5e2173 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Tue May 5 11:29:04 2026 +0200 Merge SplayTree refactor into main commit 6150be5 Merge: d794dac f5e2173 Author: Antoine du Fresne von Hohenesche <75640413+AntoineduFresne@users.noreply.github.com> Date: Tue May 5 10:43:24 2026 +0200 Merge pull request #2 from AntoineduFresne/pr/splaytree-refactor-20260505 Pr/splaytree refactor 20260505 commit f5e2173 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Tue May 5 10:42:40 2026 +0200 Prepare PR: refactor SplayTrees and update BasicDataStructure commit 6485058 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Mon May 4 19:31:31 2026 +0200 PR of the "SplayTree file BottomUP.lean" commit 67c5d4b Author: AntoineduFresne <antoine@du-fresne.ch> Date: Mon May 4 15:13:19 2026 +0200 update of BottomUp.lean commit 8b51569 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Sun May 3 11:26:16 2026 +0200 Restore φ_zig proof and apply type parameter refactoring - Updated phi_zig theorem to use BinaryTree α and Frame α type parameters - Restored linarith proof for L.empty case - Note: Type parameter refactoring exposed some issues with split cases that need further investigation Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> commit 3730e51 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Fri May 1 23:23:00 2026 +0200 Finish correctness lemmas for splayBU (descend/frame helpers, forallTree preservation, BST root preservation)\n\nCo-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> commit 040cf9c Author: AntoineduFresne <antoine@du-fresne.ch> Date: Mon Apr 27 17:51:33 2026 +0200 update commit b081a2c Author: AntoineduFresne <antoine@du-fresne.ch> Date: Mon Apr 27 17:49:20 2026 +0200 BinaryTree update commit 2309500 Author: AntoineduFresne <antoine@du-fresne.ch> Date: Mon Apr 27 17:39:57 2026 +0200 update on Splay Tree
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.