search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 297 forks source link

[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec #19188

Closed semorrison closed 1 year ago

semorrison commented 1 year ago

The @[simps] on Spec produces lemmas that aren't needed in mathlib3, and get in the way in mathlib4. This backports the removal of this attribute, to match https://github.com/leanprover-community/mathlib4/pull/5040.

Open in Gitpod

bors[bot] commented 1 year ago

:v: semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

semorrison commented 1 year ago

bors merge

semorrison commented 1 year ago

I'm removing those lemmas again, they are pointless, and cause non-confluence. If anyone would like to add such lemmas, please do it in a separate PR.

bors[bot] commented 1 year ago

Canceled.

bors[bot] commented 1 year ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.