Skip to content

chore: add iff_self to simpOnlyBuiltins - #1936

Merged
gebner merged 1 commit into
leanprover:masterfrom
kim-em:iff_self
Dec 15, 2022
Merged

gebner merged 1 commit into
leanprover:masterfrom
kim-em:iff_self

Conversation

@kim-em

@kim-em kim-em commented Dec 9, 2022

Copy link
Copy Markdown
Collaborator

This would close #1933.

@gebner

gebner commented Dec 14, 2022

Copy link
Copy Markdown
Member

Please squash the commits.

@gebner gebner added the Mathlib4 high prio Mathlib4 high priority issue label Dec 14, 2022
@kim-em

kim-em commented Dec 14, 2022

Copy link
Copy Markdown
Collaborator Author

Please squash the commits.

Squashed.

@gebner
gebner enabled auto-merge (rebase) December 14, 2022 23:04
@gebner
gebner merged commit 7c29cc7 into leanprover:master Dec 15, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Mathlib4 high prio Mathlib4 high priority issue

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Put iff_self on the "simp only nothing" list

2 participants