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

rw [decl] fails with optParams #2939

Closed
digama0 opened this issue Nov 21, 2023 · 2 comments
Closed

rw [decl] fails with optParams #2939

digama0 opened this issue Nov 21, 2023 · 2 comments
Labels
bug Something isn't working

Comments

@digama0
Copy link
Collaborator

digama0 commented Nov 21, 2023

rw does not know how to apply equation lemmas for a declaration when optParams are not set to their default values:

def foo (x := 0) : Nat := x
example : foo x = x := by simp only [foo] -- ok
example : foo x = x := by rw [foo]
-- failed to rewrite using equation theorems for 'foo'

rw [@foo] does not work either (it behaves the same, presumably because the @ needs to be applied not to foo but to the equation lemma).

@digama0 digama0 added the bug Something isn't working label Nov 21, 2023
@kmill
Copy link
Collaborator

kmill commented Dec 5, 2023

#2243 might be related

leodemoura added a commit that referenced this issue Feb 13, 2024
@leodemoura
Copy link
Member

Fixed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants