max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab_fail
History
Exact
Wojciech Różowski 793cd14b38
feat: improve message of unusedVariables linter (#13715) 
This PR improves the message of `unusedVariables` linter, by replacing
potentially confusing "unused variable `x`" message with "Variable name
`x` is not explicitly referenced. The binding can be removed (if unused)
or named `_` (if used implicitly)."

Related issue: https://github.com/leanprover/lean4/issues/13269
2026-05-13 09:40:18 +00:00
..
.gitignore chore: delete temp files before, not after tests (#12932) 2026-03-16 19:02:28 +00:00
217.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
217.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
241.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
241.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
242.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
242.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
243.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
243.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
247.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
247.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
248.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
248.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
255.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
255.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
276.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
276.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
277a.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
277a.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
277b.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
277b.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
283.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
283.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
297.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
297.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
301.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
301.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
302.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
302.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
309.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
309.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
331.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
331.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
346.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
346.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
348.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
348.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
353.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
353.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
361.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
361.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
386.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
386.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
389.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
389.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
423.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
423.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
435.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
435.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
440.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
440.lean.out.expected feat: have #eval elaborate variables (#11427) 2026-03-09 04:52:08 +00:00
448.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
448.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
449.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
449.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
450.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
450.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
496.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
496.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
550.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
550.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
586.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
586.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
593.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
593.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
621.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
621.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
641.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
641.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
653.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
653.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
655.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
655.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
689.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
689.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
690.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
690.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
697.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
697.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
755.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
755.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
770.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
770.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
799.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
799.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
906.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
906.lean.out.expected feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
916.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
916.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
995.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
995.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1007.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1007.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1011.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1011.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1038.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1038.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1050.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1050.lean.out.expected feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
1057.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1057.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1062.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1062.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1074b.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1074b.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1079.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1079.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1081.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1081.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1102.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1102.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1240.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1240.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1301.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1301.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1358.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1358.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1371.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1371.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1433.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1433.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1569.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1569.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1576.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1576.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1606.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1606.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1616.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1616.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1657.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1657.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1673.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1673.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1682.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1682.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1690.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1690.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1705.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1705.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1707.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1707.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1719.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1719.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1760.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1760.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1781.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1781.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1825.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1825.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1845.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
1845.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
1971.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
1971.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2006.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2006.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2125.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2125.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2273.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2273.lean.out.expected feat: move instance-class check to declaration site (#12325) 2026-03-06 03:23:27 +00:00
2634.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
2634.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
3989_1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
3989_1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
3989_2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
3989_2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
4117.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
4117.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
4309.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
4309.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
10488.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
10488.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ambiguousOpenExport.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ambiguousOpenExport.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
antiquotRecovery.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
antiquotRecovery.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
argNameAtPlaceholderError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
argNameAtPlaceholderError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
argNameIfMacroScopes.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
argNameIfMacroScopes.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
attrCmd.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
attrCmd.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autobound_and_macroscopes.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autobound_and_macroscopes.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundErrorMsg.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundErrorMsg.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits3.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundImplicits3.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundPostponeLoop.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoBoundPostponeLoop.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitChainNameIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitChainNameIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitCtorParamIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitCtorParamIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitForbidden.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoImplicitForbidden.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoPPExplicit.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
autoPPExplicit.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
auxDeclIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
auxDeclIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
badBinderName.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
badBinderName.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
badIhName.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
badIhName.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
beginEndAsMacro.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
beginEndAsMacro.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bigUnivOffsets.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bigUnivOffsets.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binop_at_pattern_issue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binop_at_pattern_issue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binopQuotPrecheck.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binopQuotPrecheck.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binrelTypeMismatch.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
binrelTypeMismatch.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bootstrapSorry.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
bootstrapSorry.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
byStrictIndent.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
byStrictIndent.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
calcErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
calcErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
caseSuggestions.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
caseSuggestions.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
class_def_must_fail.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
class_def_must_fail.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
classBadOutParam.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
classBadOutParam.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
collectDepsIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
collectDepsIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
commandPrefix.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
commandPrefix.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
constructorTac.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
constructorTac.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
conv1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
conv1.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
csimpAttr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
csimpAttr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ctorUnivTooBig.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ctorUnivTooBig.lean.out.expected feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
decreasing_by.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
decreasing_by.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
defaultInstance.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
defaultInstance.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
defInst.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
defInst.lean.out.expected feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
delta.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
delta.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
deprecated.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
deprecated.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
diamond1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
diamond1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
diamond5.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
diamond5.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
docStr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
docStr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
docstringLinkValidation.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
docstringLinkValidation.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
doErrorMsg.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doErrorMsg.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doIssue.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doIssue.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doLetLoop.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doLetLoop.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doNotation1.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
doNotation1.lean.out.expected fix: improve result type mismatch errors and locations in new do elaborator (#13404) 2026-04-16 09:16:27 +00:00
doSeqRightIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
doSeqRightIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
dsimpViaConst.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
dsimpViaConst.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eagerUnfoldingIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eagerUnfoldingIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ellipsisProjIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ellipsisProjIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
elseifDoErrorPos.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
elseifDoErrorPos.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
emptyc.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
emptyc.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
emptyTypeAscription.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
emptyTypeAscription.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eoi.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eoi.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eraseInsts.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eraseInsts.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
errorOnInductionForNested.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
errorOnInductionForNested.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
errorRecoveryBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
errorRecoveryBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
etaStructIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
etaStructIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eval_except.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
eval_except.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalInstMessage.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalInstMessage.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalLeak.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalLeak.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalNone.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalNone.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalSorry.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalSorry.lean.out.expected feat: have #eval elaborate variables (#11427) 2026-03-09 04:52:08 +00:00
evalWithMVar.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
evalWithMVar.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
exactErrorPos.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
exactErrorPos.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
exceptionalTrace.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
exceptionalTrace.lean.out.expected feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
exitAfterParseError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
exitAfterParseError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
failTac.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
failTac.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
file_not_found.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
file_not_found.lean.before.sh chore: delete temp files before, not after tests (#12932) 2026-03-16 19:02:28 +00:00
file_not_found.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
forErrors.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
forErrors.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
fun.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
fun.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funExpected.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funExpected.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funind_errors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funind_errors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funind_reserved.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funind_reserved.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funParen.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
funParen.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
getElem.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
getElem.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
guessLexDiff.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
guessLexDiff.lean.out.expected fix: distinguish recursive applications by source position (#13645) 2026-05-05 16:40:29 +00:00
guessLexFailures.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
guessLexFailures.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
have.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
have.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
hidingInaccessibleNames.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
hidingInaccessibleNames.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
holeErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
holeErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
holes.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
holes.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
hygienicIntro.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
hygienicIntro.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
implementedByIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implementedByIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitArgumentError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitArgumentError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitLambdaIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitLambdaIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitTypePos.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
implicitTypePos.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
indimpltarget.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
indimpltarget.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionErrors.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
inductionGen.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionGen.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionMutual.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionMutual.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionParse.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductionParse.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductive1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductive1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductiveUnivErrorMsg.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
inductiveUnivErrorMsg.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
instance1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
instance1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidFieldName.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidFieldName.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidInstImplicit.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidInstImplicit.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidMutualError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidMutualError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidNamedArgs.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidNamedArgs.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidPatternIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
invalidPatternIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
isDefEqOffsetBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
isDefEqOffsetBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
issue2260.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
issue2260.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
issue3232.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
issue3232.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
jason2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
jason2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
kernelMVarBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
kernelMVarBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letArrowOutsideDo.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letArrowOutsideDo.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letPatIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letPatIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letrec1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letrec1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letrecErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
letrecErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
liftOverLeft.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
liftOverLeft.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
linterUnusedVariables.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
linterUnusedVariables.lean.out.expected feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
longestParsePrio.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
longestParsePrio.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
loopErrorRecovery.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
loopErrorRecovery.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroElabRulesIssue2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroElabRulesIssue2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroPrio.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroPrio.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroStack.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
macroStack.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
macroSwizzle.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
macroSwizzle.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
match2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
match2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchAltIndent.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchAltIndent.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchErrorLocation.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchErrorLocation.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchErrorMsg.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchErrorMsg.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchLeftovers.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchLeftovers.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchMissingCasesAsStuckError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchMissingCasesAsStuckError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchOrIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchOrIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchUnknownFVarBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchUnknownFVarBug.lean.out.expected fix: show missing match cases in declaration order (#13266) 2026-04-03 13:33:54 +00:00
matchVarNames.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
matchVarNames.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
metaEvalInstMessage.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
metaEvalInstMessage.lean.out.expected feat: have #eval elaborate variables (#11427) 2026-03-09 04:52:08 +00:00
modBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
modBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
moduleKeywords.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
moduleKeywords.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
moduleOf.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
moduleOf.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
motiveNotTypeCorrect.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
motiveNotTypeCorrect.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mulcommErrorMessage.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mulcommErrorMessage.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
multiConstantError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
multiConstantError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mutualdef1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mutualdef1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mutwf1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mutwf1.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
mutwftypemismatch.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mutwftypemismatch.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mvarAtDefaultValue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
mvarAtDefaultValue.lean.out.expected feat: mutually dependent structure default values, and avoiding self-dependence (#12841) 2026-03-09 04:15:06 +00:00
nameArgErrorIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nameArgErrorIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
namedHoles.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
namedHoles.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
newCatPanic.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
newCatPanic.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonAtomicFieldName.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonAtomicFieldName.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonfatalattrs.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonfatalattrs.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonReserved.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
nonReserved.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
noTabs.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
noTabs.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
notationPrecheck.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
notationPrecheck.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
notNaturalNumbersGame.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
notNaturalNumbersGame.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
openExport.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
openExport.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
openScoped.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
openScoped.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
parserPrio.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
parserPrio.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
parserRecovery.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
parserRecovery.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partial_fixpoint_parseerrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partial_fixpoint_parseerrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partialIssue.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partialIssue.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partialSyntaxTraces.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partialSyntaxTraces.lean.out.expected feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
partialVariable.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
partialVariable.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
patvar.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
patvar.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap_inst_coherence.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
phashmap_inst_coherence.lean.out.expected feat: move instance-class check to declaration site (#12325) 2026-03-06 03:23:27 +00:00
ppProofs.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
ppProofs.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
precissues.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
precissues.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
private.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
private.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
protected.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
protected.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
protectedAlias.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
protectedAlias.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
pureCoeIssue.lean chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
pureCoeIssue.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
rawStringEOF.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rawStringEOF.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
redundantAlt.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
redundantAlt.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
refineFiltersOldMVars.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
refineFiltersOldMVars.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
refineOccursCheck.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
refineOccursCheck.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
renameBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
renameBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
replaceLocalDeclInstantiateMVars.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
replaceLocalDeclInstantiateMVars.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rewrite.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
rewrite.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
root.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
root.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
run_meta1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
run_meta1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
run_test.sh chore: check test output before exit code in piles (#12947) 2026-03-17 16:34:21 +00:00
runTacticMustCatchExceptions.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
runTacticMustCatchExceptions.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rwWithSynthesizeBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
rwWithSynthesizeBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
sanitychecks.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
sanitychecks.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scientific.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scientific.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedInstanceOutsideNamespace.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedInstanceOutsideNamespace.lean.out.expected feat: move instance-class check to declaration site (#12325) 2026-03-06 03:23:27 +00:00
scopedLocalInsts.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedLocalInsts.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedMacros.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedMacros.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedTokens.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
scopedTokens.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
semicolonOrLinebreak.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
semicolonOrLinebreak.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
setLit.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
setLit.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
shadow.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
shadow.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
simp_trace.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
simp_trace.lean.out.expected chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
simpArgTypeMismatch.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
simpArgTypeMismatch.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
sorryAtError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
sorryAtError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
specializeAttr.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
specializeAttr.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
string_gaps_err_newline.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
string_gaps_err_newline.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
struct1.lean feat: mutually dependent structure default values, and avoiding self-dependence (#12841) 2026-03-09 04:15:06 +00:00
struct1.lean.out.expected feat: mutually dependent structure default values, and avoiding self-dependence (#12841) 2026-03-09 04:15:06 +00:00
structAutoBound.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structAutoBound.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structDefault.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structDefault.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structDefValueOverride.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structDefValueOverride.lean.out.expected feat: mutually dependent structure default values, and avoiding self-dependence (#12841) 2026-03-09 04:15:06 +00:00
structInst1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structInst1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structInstError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structInstError.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structSorryBug.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
structSorryBug.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StxQuot.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
StxQuot.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
substFails.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
substFails.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
syntaxErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
syntaxErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
syntaxPrec.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
syntaxPrec.lean.out.expected feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
syntheticHolesAsPatterns.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
syntheticHolesAsPatterns.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
synthorder.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
synthorder.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tacUnsolvedGoalsErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tacUnsolvedGoalsErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tcloop.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tcloop.lean.out.expected feat: move instance-class check to declaration site (#12325) 2026-03-06 03:23:27 +00:00
termination_by.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
termination_by.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
termination_by_vars.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
termination_by_vars.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
terminationFailure.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
terminationFailure.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
test_extern.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
test_extern.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
theoremType.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
theoremType.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tokenErrors.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tokenErrors.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tooManyVarsAtInduction.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
tooManyVarsAtInduction.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trailingComma.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
trailingComma.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeIncorrectPat.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeIncorrectPat.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeMismatch.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeMismatch.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeOf.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
typeOf.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unfoldFailure.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unfoldFailure.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
univInference.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
univInference.lean.out.expected feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
unknownCannotBeComplex.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unknownCannotBeComplex.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unknownId.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unknownId.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unknownTactic.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unknownTactic.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unsolvedIndCases.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unsolvedIndCases.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unused_univ.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
unused_univ.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
versoDocMissing.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
versoDocMissing.lean.out.expected feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures (#12597) 2026-03-10 10:59:13 +00:00
warningAsError.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
warningAsError.lean.out.expected feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
wf1.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wf1.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wf2.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wf2.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wildcardAlt.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
wildcardAlt.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
withLocationImplementationDetails.lean chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00
withLocationImplementationDetails.lean.out.expected chore: switch to new test/bench suite (#12590) 2026-02-25 13:51:53 +00:00