[Merged by Bors] - chore: fix tests after #6528 disabled autoimplicits#6597
[Merged by Bors] - chore: fix tests after #6528 disabled autoimplicits#6597
Conversation
|
✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with |
Can you open an issue for each of these two, and reference it in a TODO comment? |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
I was planning to look into them/discuss on zulip myself before reporting. I think that should be enough, we can always add the comments later if it does turn out they should become issues |
|
bors r+ |
These work on the command line and therefore didn't fail in CI (as `lake env lean blah.lean` doesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors. I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file. This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat. Two files had issues, that we may want to follow up on `test/superscript.lean` which failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional). And the `ToExpr` deriving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
These work on the command line and therefore didn't fail in CI (as `lake env lean blah.lean` doesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors. I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file. This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat. Two files had issues, that we may want to follow up on `test/superscript.lean` which failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional). And the `ToExpr` deriving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.
These work on the command line and therefore didn't fail in CI (as
lake env lean blah.leandoesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors.I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file.
This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat.
Two files had issues, that we may want to follow up on
test/superscript.leanwhich failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional).And the
ToExprderiving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.