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

feat: expose Kernel.check for debugging purposes #5412

Merged
merged 1 commit into from
Oct 1, 2024
Merged

feat: expose Kernel.check for debugging purposes #5412

merged 1 commit into from
Oct 1, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Sep 21, 2024

along Kernel.isDefEq and Kernel.whnf.

@nomeata
feat: expose Kernel.check for debugging purposes
0a44c68 
along `Kernel.isDefEq` and `Kernel.whnf`.
@nomeata nomeata force-pushed the joachim/Kernel.check branch from 86d2e0d to 0a44c68 Compare September 21, 2024 09:55
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 21, 2024 10:11 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 21, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5412
6b61c46
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5412
21cae62
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 21, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@nomeata
Copy link
Collaborator Author

nomeata commented Sep 25, 2024

(Closing until I actually need this.)

@nomeata nomeata closed this Sep 25, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Oct 1, 2024

This maybe might have saved me some debugging time today, so probably worth having.

@nomeata nomeata reopened this Oct 1, 2024
@nomeata nomeata marked this pull request as ready for review October 1, 2024 21:09
@nomeata nomeata requested a review from leodemoura as a code owner October 1, 2024 21:09
@nomeata nomeata enabled auto-merge October 1, 2024 21:10
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 1, 2024 21:24 Inactive
@nomeata nomeata added this pull request to the merge queue Oct 1, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5412
8af7853
Merged via the queue into master with commit e417a23 Oct 1, 2024
30 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-bot