Skip to content

chore: fixes for leanprover/lean4#2734#316

Closed
kim-em wants to merge 9 commits intomainfrom
lean-pr-testing-2734
Closed

chore: fixes for leanprover/lean4#2734#316
kim-em wants to merge 9 commits intomainfrom
lean-pr-testing-2734

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Oct 23, 2023

This is stacked on top of #297.

@kim-em kim-em added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on core changes This PR need only be reviewed after changes land in Lean core. labels Oct 23, 2023
@kim-em kim-em changed the title fixes for leanprover/lean4#2734 chore: fixes for leanprover/lean4#2734 Oct 23, 2023
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Copy link
Copy Markdown
Contributor

@joehendrix joehendrix left a comment

Choose a reason for hiding this comment

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

The changes look good to me.

@kim-em kim-em added v4.3.0-rc1 merged-into-nightly-testing This has been merged into `nightly-testing`, and will join `main` when we update the toolchain. labels Oct 25, 2023
kim-em added a commit that referenced this pull request Oct 26, 2023
@digama0 digama0 closed this in 0daeae3 Oct 31, 2023
@digama0 digama0 deleted the lean-pr-testing-2734 branch October 31, 2023 05:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on core changes This PR need only be reviewed after changes land in Lean core. merged-into-nightly-testing This has been merged into `nightly-testing`, and will join `main` when we update the toolchain.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants