-
Notifications
You must be signed in to change notification settings - Fork 415
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.
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
RFC: remove simpCtorEq
from the default simprocs
#5046
Comments
Side note: |
leodemoura
added a commit
that referenced
this issue
Aug 26, 2024
The simproc is renamed to `reduceCtorEq`. closes #5046
leodemoura
added a commit
that referenced
this issue
Aug 26, 2024
The simproc is renamed to `reduceCtorEq`. closes #5046
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Proposal
Currently
simp only
simplifies an equalitya = b
toFalse
, ifa
andb
are different constructors for an inductive type. This is apparently done by theMeta.Simp.simpCtorEq
simproc.Would it be possible to turn off this
simproc
insimp only
, while still keeping it in the set of rules used bysimp
? Here are three arguments in favour of this change:The
simpCtorEq
simproc is applicable to the first and last of these goals but not to the middle one.simp only
, where it is (AFAICT) impossible to turn off. For example, the simp tactic is used internally in the Mathlibring
tactic to clean up failures before they are presented to the user. This simproc actually cleans up some failures too aggressively, so that the information to the user is lost!Community Feedback
Discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20only.20on.20numeric.20goals
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: