Skip to content
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

omega does not look through abbreviations in types #5733

Open
nomeata opened this issue Oct 16, 2024 · 0 comments
Open

omega does not look through abbreviations in types #5733

nomeata opened this issue Oct 16, 2024 · 0 comments
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@nomeata
Copy link
Contributor

nomeata commented Oct 16, 2024

I would expect this to work

example (x : Fin 3) : x ≠ x + 1 := by omega

abbrev Foo := Fin 3

/--
error: omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
-/
#guard_msgs in
example (x : Foo) : x ≠ x + 1 := by omega

without this, I get penalized for introducing nice names for some of my abstractions. Most other parts of the system can look through abbreviations (e.g. name resolution, type class inference), so omega should maybe too.

Probably just a matter of calling whnfR in the right place.

Versions

"4.12.0-nightly-2024-10-15"

Additional Information

Wanted to use this in teorth/equational_theories#599.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

@nomeata nomeata added the bug Something isn't working label Oct 16, 2024
@nomeata nomeata changed the title omega does not look abbreviations in types omega does not look through abbreviations in types Oct 16, 2024
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Oct 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Development

No branches or pull requests

2 participants