Skip to content

chore: add iff_self to simpOnlyBuiltins#1936

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

chore: add iff_self to simpOnlyBuiltins#1936
gebner merged 1 commit intoleanprover:masterfrom
kim-em:iff_self

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

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

This would close #1933.

@gebner
Copy link
Copy Markdown
Member

gebner commented Dec 14, 2022

Please squash the commits.

@gebner gebner added the Mathlib4 high prio Mathlib4 high priority issue label Dec 14, 2022
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Dec 14, 2022

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