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: add #print opaques command #966

Merged
merged 8 commits into from
Dec 22, 2024
Merged

feat: add #print opaques command #966

merged 8 commits into from
Dec 22, 2024

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Sep 27, 2024 •
edited
Loading

Adds the #print opaques command that shows all computationally relevant opaque and partial definitions that a function depends on.

Co-authored-by: Mario Carneiro di.gama@gmail.com

@fgdorais fgdorais added the WIP work in progress label Sep 27, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 27, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#966
a407dd5
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Sep 27, 2024 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
a8bacfa
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
c017932
@fgdorais fgdorais marked this pull request as ready for review November 22, 2024 23:55
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed WIP work in progress labels Nov 22, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
8caf321
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 23, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
2587ef2
@fgdorais fgdorais added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label Dec 18, 2024
@fgdorais fgdorais requested review from kim-em and mattrobball and removed request for kim-em December 18, 2024 06:10
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 21, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
f8234b4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#966
906dc95
@fgdorais fgdorais added this pull request to the merge queue Dec 22, 2024
Merged via the queue into main with commit f007bfe Dec 22, 2024
3 checks passed
@github-actions github-actions bot removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

@mattrobball mattrobball mattrobball approved these changes

Assignees
No one assigned
Labels
builds-mathlib will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@fgdorais @leanprover-community-bot @digama0 @mattrobball