Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Plane trees #1110

Merged
merged 7 commits into from Apr 13, 2024
Merged

Plane trees #1110

merged 7 commits into from Apr 13, 2024

Conversation

EgbertRijke
Copy link
Collaborator

This is a short pull request introducing plane trees and proves that the type of plane trees is equivalent to the type of full binary trees.

There are some related old files about binary trees which I will clean up in another pull request, but not here.

VojtechStep
VojtechStep reviewed Apr 12, 2024
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That was quick 😅

src/trees/plane-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/full-binary-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/full-binary-trees.lagda.md Outdated Show resolved Hide resolved
VojtechStep
VojtechStep reviewed Apr 12, 2024
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few typos, then it's good to merge 👌

src/trees/full-binary-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/full-binary-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/plane-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/full-binary-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/plane-trees.lagda.md Outdated Show resolved Hide resolved
src/trees/plane-trees.lagda.md Outdated Show resolved Hide resolved
@EgbertRijke EgbertRijke mentioned this pull request Apr 13, 2024
Merged
@VojtechStep VojtechStep enabled auto-merge (squash) April 13, 2024 16:14
@VojtechStep VojtechStep enabled auto-merge (squash) April 13, 2024 16:15
@VojtechStep
Copy link
Collaborator

Looks good, enabling automerge

@VojtechStep VojtechStep merged commit aab86e6 into UniMath:master Apr 13, 2024
4 checks passed
fredrik-bakke pushed a commit that referenced this pull request Apr 17, 2024
@EgbertRijke
Hereditary W-types (#1112)
6fb97c0 
In this PR I generalized the equivalence constructed in #1110, to
something that I called "hereditary W-types". This PR is independent of
#1110.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@VojtechStep VojtechStep VojtechStep left review comments

Assignees
No one assigned
Labels
trees
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@EgbertRijke @VojtechStep