mathlib3
[Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file
#19223
Closed
Overview
Commits
2
Changes
View On GitHub

[Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file #19223

urkud wants to merge 2 commits into master from YK-simp-attrs
urkud
urkud Snapshot
e7ac51a1
urkud urkud requested a review 2 years ago
urkud urkud requested a review 2 years ago
github-actions github-actions added modifies-synchronized-file
urkud urkud added awaiting-review
urkud urkud added mathport
urkud Fix a test
c5e064ee
fpvandoorn
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
urkud
bors
bors bors changed the title refactor(*): move all `mk_simp_attribute` commands to 1 file [Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file 2 years ago
bors bors closed this 2 years ago
bors bors deleted the YK-simp-attrs branch 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge mathport modifies-synchronized-file
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum