Commit 2023-08-15 23:11 3045aef4

chore: fix tests after #6528 disabled autoimplicits (#6597) 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.