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

chore: remove Std.Data.List import from Omega #568

Merged
merged 3 commits into from
Feb 1, 2024
Merged

chore: remove Std.Data.List import from Omega #568

merged 3 commits into from
Feb 1, 2024

Conversation

joehendrix
Copy link
Contributor

@joehendrix joehendrix commented Jan 29, 2024 •
edited
Loading

This adds lemmas to Std.Data.List from Omega dependencies so that Omega can be used in List lemmas.

I changed a few proofs as part of this to reduce dependencies and include fewer lemmas in Init.

@joehendrix joehendrix requested a review from kim-em January 29, 2024 23:42
kim-em
kim-em reviewed Jan 30, 2024
View reviewed changes
Copy link
Collaborator

@kim-em kim-em left a comment

Choose a reason for hiding this comment

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

Looks good to me.

There are lots of theorems in Std.Tactic.Omega.MinNatAbs that are not actually used (they are leftovers from the verified version), but I don't think them removing them actually reduces how much we need to move to Init, in any case.

@joehendrix joehendrix added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label Jan 30, 2024
@joehendrix joehendrix merged commit 0b89788 into main Feb 1, 2024
2 checks passed
@joehendrix joehendrix deleted the jhx/omega_init_list branch February 1, 2024 04:38
fgdorais pushed a commit to fgdorais/batteries that referenced this pull request Feb 18, 2024
@joehendrix @kim-em @fgdorais
chore: remove Std.Data.List import from Omega (leanprover-community#568)
42e2c40 
Co-authored-by: Scott Morrison <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
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.
3 participants
@joehendrix @kim-em @digama0