search

leanprover-community / quote4

Intuitive, type-safe expression quotations for Lean 4.
Apache License 2.0
73 stars 11 forks source link

linter.constructorNameAsVariable false in turnExistsIntoForall #52

Open awalterschulze opened 3 weeks ago

awalterschulze commented 3 weeks ago

Amazing library, thanks so much for the amazing work.

We are just attempting to update and we are having a problem:

In https://github.com/leanprover-community/quote4/pull/49 the option was added set_option linter.constructorNameAsVariable false in above the test for turnExistsIntoForall.

We use Qoute4 on exists here https://github.com/katydid/proofs/blob/main/Katydid/Std/Balistic.lean#L283 in a tactic called wreck_exists, but we get this error: error: ././././Katydid/Std/Balistic.lean:280:0: unknown free variable '_fvar.33580'

When we use set_option linter.constructorNameAsVariable false in above then the tactic is not created, the error goes away, but we cannot use wreck_exists anymore, because we get error: ././././Katydid/Std/Balistic.lean:326:31: unknown tactic

This is where we are attempting to upgrade to the newest version of lean and it is breaking https://github.com/katydid/proofs/pull/86/commits/3789860217369e59aefbbe6136fb0169c62a8526#diff-d996139c0cef6f145df4d12efca1d12573666cd1b14e87d1ba4e4addf7fd2949R279

I hope this is a useful issue report.

awalterschulze commented 3 weeks ago

I found a temporary work around https://github.com/katydid/proofs/pull/86/commits/33c67f55ed9080c46d857778c38a5fbb53606895

But it would still be great to get this lint error fixed, so I hope it is worth keeping the issue open, until a fix is found