| .. |
|
docparse
|
chore: rename String.ValidPos to String.Pos (#11240)
|
2025-11-24 16:40:21 +00:00 |
|
grind
|
feat: cleanup denominators in grind linarith (#11375)
|
2025-11-26 05:21:55 +00:00 |
|
interactive
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
Reformat
|
|
|
|
run
|
chore: restore set_library_suggestions tests after update-stage0
|
2025-11-29 01:08:47 +11:00 |
|
server
|
test: improve language server test coverage (#10574)
|
2025-09-30 11:15:03 +00:00 |
|
trust0
|
|
|
|
.gitignore
|
|
|
|
217.lean
|
|
|
|
217.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
220.lean
|
|
|
|
220.lean.expected.out
|
|
|
|
223.lean
|
|
|
|
223.lean.expected.out
|
|
|
|
236.lean
|
feat: top-down heuristic delaboration
|
2021-08-03 09:13:18 +02:00 |
|
236.lean.expected.out
|
|
|
|
241.lean
|
|
|
|
241.lean.expected.out
|
|
|
|
242.lean
|
feat: add unicode(...) parser syntax and pp.unicode option (#10373)
|
2025-09-14 04:40:03 +00:00 |
|
242.lean.expected.out
|
feat: add unicode(...) parser syntax and pp.unicode option (#10373)
|
2025-09-14 04:40:03 +00:00 |
|
243.lean
|
fix: fixes #243
|
2021-05-03 13:01:16 -07:00 |
|
243.lean.expected.out
|
|
|
|
247.lean
|
|
|
|
247.lean.expected.out
|
|
|
|
248.lean
|
|
|
|
248.lean.expected.out
|
|
|
|
255.lean
|
feat: allow hygienic capture of section variables in quotations
|
2021-01-24 11:46:04 -08:00 |
|
255.lean.expected.out
|
|
|
|
276.lean
|
|
|
|
276.lean.expected.out
|
feat: add option pp.piBinderNames (#10374)
|
2025-09-14 05:15:04 +00:00 |
|
277a.lean
|
|
|
|
277a.lean.expected.out
|
|
|
|
277b.lean
|
|
|
|
277b.lean.expected.out
|
|
|
|
283.lean
|
|
|
|
283.lean.expected.out
|
|
|
|
297.lean
|
|
|
|
297.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
301.lean
|
|
|
|
301.lean.expected.out
|
|
|
|
302.lean
|
|
|
|
302.lean.expected.out
|
|
|
|
307.lean
|
chore: remove >6 month old deprecations (#10446)
|
2025-09-22 12:47:11 +00:00 |
|
307.lean.expected.out
|
|
|
|
309.lean
|
|
|
|
309.lean.expected.out
|
|
|
|
331.lean
|
feat: allow optional type in example
|
2022-09-13 03:11:04 -07:00 |
|
331.lean.expected.out
|
|
|
|
345.lean.expected.out
|
|
|
|
346.lean
|
|
|
|
346.lean.expected.out
|
fix: deprecation warning location with field notation (#10826)
|
2025-10-23 20:55:25 +00:00 |
|
348.lean
|
|
|
|
348.lean.expected.out
|
|
|
|
353.lean
|
|
|
|
353.lean.expected.out
|
feat: prioritize stuck synthetic MVar problems to improve error messages (#11184)
|
2025-11-16 00:09:48 +00:00 |
|
361.lean
|
|
|
|
361.lean.expected.out
|
|
|
|
366.lean
|
|
|
|
366.lean.expected.out
|
|
|
|
386.lean
|
|
|
|
386.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
389.lean
|
|
|
|
389.lean.expected.out
|
|
|
|
414.lean
|
|
|
|
414.lean.expected.out
|
|
|
|
415.lean
|
|
|
|
415.lean.expected.out
|
|
|
|
421.lean
|
|
|
|
421.lean.expected.out
|
|
|
|
423.lean
|
|
|
|
423.lean.expected.out
|
|
|
|
435.lean
|
fix: fixes #435
|
2021-05-02 18:16:57 -07:00 |
|
435.lean.expected.out
|
|
|
|
435b.lean
|
|
|
|
435b.lean.expected.out
|
|
|
|
439.lean.expected.out
|
|
|
|
440.lean
|
|
|
|
440.lean.expected.out
|
|
|
|
445.lean
|
|
|
|
445.lean.expected.out
|
|
|
|
448.lean
|
|
|
|
448.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
449.lean
|
|
|
|
449.lean.expected.out
|
|
|
|
450.lean
|
|
|
|
450.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
469.lean
|
|
|
|
469.lean.expected.out
|
|
|
|
474.lean
|
|
|
|
474.lean.expected.out
|
|
|
|
490.lean
|
|
|
|
490.lean.expected.out
|
|
|
|
496.lean
|
|
|
|
496.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
529.lean
|
|
|
|
529.lean.expected.out
|
|
|
|
550.lean
|
|
|
|
550.lean.expected.out
|
|
|
|
586.lean
|
|
|
|
586.lean.expected.out
|
|
|
|
593.lean
|
fix: fixes #593
|
2021-08-02 10:46:12 -07:00 |
|
593.lean.expected.out
|
|
|
|
603.lean.expected.out
|
|
|
|
604.lean
|
|
|
|
604.lean.expected.out
|
|
|
|
620.lean
|
|
|
|
620.lean.expected.out
|
|
|
|
621.lean
|
|
|
|
621.lean.expected.out
|
|
|
|
625.lean
|
|
|
|
625.lean.expected.out
|
|
|
|
641.lean
|
|
|
|
641.lean.expected.out
|
|
|
|
653.lean
|
|
|
|
653.lean.expected.out
|
|
|
|
655.lean
|
|
|
|
655.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
679.lean
|
|
|
|
679.lean.expected.out
|
|
|
|
689.lean
|
|
|
|
689.lean.expected.out
|
|
|
|
690.lean
|
|
|
|
690.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
697.lean
|
|
|
|
697.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
714.lean
|
feat: make sure #check produces some result even when there are pending TC problems
|
2021-10-06 13:37:06 -07:00 |
|
714.lean.expected.out
|
|
|
|
755.lean
|
|
|
|
755.lean.expected.out
|
|
|
|
770.lean
|
|
|
|
770.lean.expected.out
|
|
|
|
799.lean
|
|
|
|
799.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
801.lean
|
|
|
|
801.lean.expected.out
|
|
|
|
813.lean
|
|
|
|
813.lean.expected.out
|
|
|
|
815b.lean
|
|
|
|
815b.lean.expected.out
|
feat: suppress safe shadowing within fun binders (#10376)
|
2025-09-14 15:54:59 +00:00 |
|
906.lean
|
|
|
|
906.lean.expected.out
|
|
|
|
916.lean
|
|
|
|
916.lean.expected.out
|
|
|
|
948.lean
|
|
|
|
948.lean.expected.out
|
|
|
|
951.lean
|
|
|
|
951.lean.expected.out
|
|
|
|
973.lean
|
|
|
|
973.lean.expected.out
|
|
|
|
973b.lean
|
|
|
|
973b.lean.expected.out
|
|
|
|
995.lean
|
|
|
|
995.lean.expected.out
|
|
|
|
1007.lean
|
|
|
|
1007.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
1011.lean
|
|
|
|
1011.lean.expected.out
|
feat: improve error when an identifier is unbound because autoImplicit is off (#11119)
|
2025-11-19 03:11:34 +00:00 |
|
1021.lean
|
|
|
|
1021.lean.expected.out
|
chore: remove redundant imports in core (#10750)
|
2025-10-16 20:27:46 +00:00 |
|
1027.lean
|
fix: simp_all was "self-simplifying" simplified hypotheses
|
2022-02-23 16:48:28 -08:00 |
|
1027.lean.expected.out
|
|
|
|
1038.lean
|
|
|
|
1038.lean.expected.out
|
fix: deprecation warning location with field notation (#10826)
|
2025-10-23 20:55:25 +00:00 |
|
1039.lean
|
feat: auto-completion for end names (#10660)
|
2025-10-08 11:12:05 +00:00 |
|
1039.lean.expected.out
|
|
|
|
1050.lean
|
|
|
|
1050.lean.expected.out
|
|
|
|
1057.lean
|
|
|
|
1057.lean.expected.out
|
fix: preserve error locations when expanding match arms (#10783)
|
2025-10-15 13:31:42 +00:00 |
|
1062.lean
|
|
|
|
1062.lean.expected.out
|
|
|
|
1074b.lean
|
|
|
|
1074b.lean.expected.out
|
|
|
|
1079.lean
|
chore: eliminate uses of intros x y z (#9983)
|
2025-08-19 06:09:13 +00:00 |
|
1079.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
1081.lean
|
|
|
|
1081.lean.expected.out
|
|
|
|
1098.lean
|
|
|
|
1098.lean.expected.out
|
|
|
|
1102.lean
|
|
|
|
1102.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
1112.lean
|
|
|
|
1112.lean.expected.out
|
|
|
|
1113.lean
|
|
|
|
1113.lean.expected.out
|
|
|
|
1163.lean.expected.out
|
|
|
|
1206.lean
|
|
|
|
1206.lean.expected.out
|
|
|
|
1235.lean
|
|
|
|
1235.lean.expected.out
|
|
|
|
1240.lean
|
|
|
|
1240.lean.expected.out
|
|
|
|
1275.lean
|
|
|
|
1275.lean.expected.out
|
perf: make macro scope numbering less dependent on surrounding context (#10027)
|
2025-08-22 13:16:02 +00:00 |
|
1279.lean
|
|
|
|
1279.lean.expected.out
|
|
|
|
1279_simplified.lean
|
|
|
|
1279_simplified.lean.expected.out
|
|
|
|
1292.lean
|
|
|
|
1292.lean.expected.out
|
|
|
|
1298.lean
|
|
|
|
1298.lean.expected.out
|
|
|
|
1301.lean
|
|
|
|
1301.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
1321.lean
|
|
|
|
1321.lean.expected.out
|
feat: overhaul meta system (#10362)
|
2025-09-17 21:04:29 +00:00 |
|
1358.lean
|
|
|
|
1358.lean.expected.out
|
|
|
|
1363.lean
|
chore: rename String.ValidPos to String.Pos (#11240)
|
2025-11-24 16:40:21 +00:00 |
|
1363.lean.expected.out
|
|
|
|
1367.lean
|
|
|
|
1367.lean.expected.out
|
|
|
|
1371.lean
|
|
|
|
1371.lean.expected.out
|
|
|
|
1377.lean
|
|
|
|
1377.lean.expected.out
|
|
|
|
1433.lean
|
|
|
|
1433.lean.expected.out
|
|
|
|
1569.lean
|
|
|
|
1569.lean.expected.out
|
|
|
|
1571.lean
|
|
|
|
1571.lean.expected.out
|
|
|
|
1576.lean
|
|
|
|
1576.lean.expected.out
|
|
|
|
1606.lean
|
|
|
|
1606.lean.expected.out
|
|
|
|
1616.lean
|
|
|
|
1616.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
1657.lean
|
|
|
|
1657.lean.expected.out
|
|
|
|
1668.lean
|
|
|
|
1668.lean.expected.out
|
|
|
|
1673.lean
|
|
|
|
1673.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
1681.lean
|
|
|
|
1681.lean.expected.out
|
|
|
|
1682.lean
|
|
|
|
1682.lean.expected.out
|
|
|
|
1690.lean
|
|
|
|
1690.lean.expected.out
|
|
|
|
1705.lean
|
|
|
|
1705.lean.expected.out
|
|
|
|
1707.lean
|
|
|
|
1707.lean.expected.out
|
|
|
|
1719.lean
|
|
|
|
1719.lean.expected.out
|
|
|
|
1760.lean
|
|
|
|
1760.lean.expected.out
|
|
|
|
1763.lean
|
|
|
|
1763.lean.expected.out
|
|
|
|
1779.lean
|
|
|
|
1779.lean.expected.out
|
|
|
|
1781.lean
|
|
|
|
1781.lean.expected.out
|
|
|
|
1804.lean
|
|
|
|
1804.lean.expected.out
|
|
|
|
1825.lean
|
|
|
|
1825.lean.expected.out
|
|
|
|
1845.lean
|
|
|
|
1845.lean.expected.out
|
|
|
|
1856.lean
|
|
|
|
1856.lean.expected.out
|
|
|
|
1878.lean
|
|
|
|
1878.lean.expected.out
|
|
|
|
1891.lean
|
|
|
|
1891.lean.expected.out
|
|
|
|
1918.lean
|
|
|
|
1918.lean.expected.out
|
|
|
|
1971.lean
|
|
|
|
1971.lean.expected.out
|
|
|
|
2005.lean
|
fix: be more careful with MatchResult.uncovered in syntax match
|
2023-01-09 13:05:00 +01:00 |
|
2005.lean.expected.out
|
|
|
|
2006.lean
|
|
|
|
2006.lean.expected.out
|
|
|
|
2045.lean
|
|
|
|
2045.lean.expected.out
|
|
|
|
2077.lean
|
|
|
|
2077.lean.expected.out
|
|
|
|
2115.lean
|
|
|
|
2115.lean.expected.out
|
|
|
|
2125.lean
|
|
|
|
2125.lean.expected.out
|
|
|
|
2178.lean
|
|
|
|
2178.lean.expected.out
|
|
|
|
2273.lean
|
|
|
|
2273.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
2361.lean
|
|
|
|
2361.lean.expected.out
|
|
|
|
2505.lean
|
|
|
|
2505.lean.expected.out
|
|
|
|
2514.lean
|
|
|
|
2514.lean.expected.out
|
|
|
|
2634.lean
|
|
|
|
2634.lean.expected.out
|
|
|
|
3057.lean
|
feat: .ctorIdx for all inductives (#9951)
|
2025-08-25 10:47:06 +00:00 |
|
3057.lean.expected.out
|
|
|
|
3140.lean
|
|
|
|
3140.lean.expected.out
|
|
|
|
3989_1.lean
|
|
|
|
3989_1.lean.expected.out
|
|
|
|
3989_2.lean
|
|
|
|
3989_2.lean.expected.out
|
|
|
|
4089.lean
|
|
|
|
4089.lean.expected.out
|
perf: sort before elim dead branches (#11366)
|
2025-11-27 22:21:06 +00:00 |
|
4117.lean
|
|
|
|
4117.lean.expected.out
|
|
|
|
4240.lean
|
|
|
|
4240.lean.expected.out
|
perf: sort before elim dead branches (#11366)
|
2025-11-27 22:21:06 +00:00 |
|
4309.lean
|
|
|
|
4309.lean.expected.out
|
|
|
|
4375.lean
|
|
|
|
4375.lean.expected.out
|
|
|
|
4452.lean
|
|
|
|
4452.lean.expected.out
|
|
|
|
4591.lean
|
|
|
|
4591.lean.expected.out
|
feat: "try this" messages with support for interactivity (#10524)
|
2025-10-13 13:39:03 +00:00 |
|
4845.lean
|
|
|
|
4845.lean.expected.out
|
|
|
|
6601.lean
|
|
|
|
6601.lean.expected.out
|
|
|
|
10488.lean
|
feat: improve error messages for ambiguous 3.toDecmial syntax (#10488)
|
2025-09-26 01:12:10 +00:00 |
|
10488.lean.expected.out
|
feat: improve error messages for ambiguous 3.toDecmial syntax (#10488)
|
2025-09-26 01:12:10 +00:00 |
|
abst.lean
|
|
|
|
abst.lean.expected.out
|
|
|
|
allFieldForConstants.lean
|
|
|
|
allFieldForConstants.lean.expected.out
|
|
|
|
ambiguousOpenExport.lean
|
|
|
|
ambiguousOpenExport.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
antiquotRecovery.lean
|
|
|
|
antiquotRecovery.lean.expected.out
|
|
|
|
appParserIssue.lean
|
refactor: remove optional leading pipe from match, use many1Indent instead of sepBy1
|
2020-12-16 18:27:05 +01:00 |
|
appParserIssue.lean.expected.out
|
|
|
|
argNameAtPlaceholderError.lean
|
|
|
|
argNameAtPlaceholderError.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
argNameIfMacroScopes.lean
|
|
|
|
argNameIfMacroScopes.lean.expected.out
|
|
|
|
arrayGetU.lean
|
chore: remove >6 month old deprecations (#10446)
|
2025-09-22 12:47:11 +00:00 |
|
arrayGetU.lean.expected.out
|
|
|
|
attrCmd.lean
|
|
|
|
attrCmd.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
autobound_and_macroscopes.lean
|
|
|
|
autobound_and_macroscopes.lean.expected.out
|
|
|
|
autoBoundErrorMsg.lean
|
test: add test for former weird error message
|
2021-03-23 18:16:06 -07:00 |
|
autoBoundErrorMsg.lean.expected.out
|
|
|
|
autoBoundImplicits1.lean
|
|
|
|
autoBoundImplicits1.lean.expected.out
|
feat: improve error when an identifier is unbound because autoImplicit is off (#11119)
|
2025-11-19 03:11:34 +00:00 |
|
autoBoundImplicits2.lean
|
|
|
|
autoBoundImplicits2.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
autoBoundImplicits3.lean
|
feat: improve error when an identifier is unbound because autoImplicit is off (#11119)
|
2025-11-19 03:11:34 +00:00 |
|
autoBoundImplicits3.lean.expected.out
|
feat: improve error when an identifier is unbound because autoImplicit is off (#11119)
|
2025-11-19 03:11:34 +00:00 |
|
autoBoundPostponeLoop.lean
|
fix: nontermination
|
2021-03-18 14:23:03 -07:00 |
|
autoBoundPostponeLoop.lean.expected.out
|
|
|
|
autoImplicitChain.lean
|
|
|
|
autoImplicitChain.lean.expected.out
|
|
|
|
autoImplicitChainNameIssue.lean
|
|
|
|
autoImplicitChainNameIssue.lean.expected.out
|
|
|
|
autoImplicitCtorParamIssue.lean
|
fix: auto implicit behavior on constructors
|
2022-05-04 15:04:49 -07:00 |
|
autoImplicitCtorParamIssue.lean.expected.out
|
|
|
|
autoImplicitForbidden.lean
|
|
|
|
autoImplicitForbidden.lean.expected.out
|
|
|
|
autoIssue.lean
|
feat: structure instance notation elaboration improvements (#7717)
|
2025-03-30 17:40:36 +00:00 |
|
autoIssue.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
autoPPExplicit.lean
|
|
|
|
autoPPExplicit.lean.expected.out
|
|
|
|
auxDeclIssue.lean
|
|
|
|
auxDeclIssue.lean.expected.out
|
|
|
|
badBinderName.lean
|
|
|
|
badBinderName.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
badIhName.lean
|
|
|
|
badIhName.lean.expected.out
|
|
|
|
baseIO.lean
|
chore: reenable subset of new-compiler tests and delete others
|
2025-06-20 17:29:10 +02:00 |
|
baseIO.lean.expected.out
|
feat: zero cost BaseIO (#10625)
|
2025-10-22 10:55:12 +02:00 |
|
beginEndAsMacro.lean
|
|
|
|
beginEndAsMacro.lean.expected.out
|
|
|
|
bigUnivOffsets.lean
|
|
|
|
bigUnivOffsets.lean.expected.out
|
|
|
|
binder_predicates.lean
|
chore: upstream Std.Util.ExtendedBinders (#3320)
|
2024-02-14 11:36:00 +00:00 |
|
binder_predicates.lean.expected.out
|
|
|
|
binderCacheIssue.lean
|
|
|
|
binderCacheIssue.lean.expected.out
|
|
|
|
binderCacheIssue2.lean
|
|
|
|
binderCacheIssue2.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
bindersAbstractingUnassignedMVars.lean
|
|
|
|
bindersAbstractingUnassignedMVars.lean.expected.out
|
|
|
|
binop_at_pattern_issue.lean
|
|
|
|
binop_at_pattern_issue.lean.expected.out
|
|
|
|
binop_lazy.lean
|
|
|
|
binop_lazy.lean.expected.out
|
|
|
|
binopInfoTree.lean
|
|
|
|
binopInfoTree.lean.expected.out
|
fix: detect private references in inferred type of public def (#10762)
|
2025-10-15 12:51:54 +00:00 |
|
binopQuotPrecheck.lean
|
|
|
|
binopQuotPrecheck.lean.expected.out
|
|
|
|
binrel_binop.lean
|
|
|
|
binrel_binop.lean.expected.out
|
|
|
|
binrelTypeMismatch.lean
|
|
|
|
binrelTypeMismatch.lean.expected.out
|
|
|
|
binsearch.lean
|
|
|
|
binsearch.lean.expected.out
|
|
|
|
bintreeGoal.lean
|
|
|
|
bintreeGoal.lean.expected.out
|
|
|
|
bitwise.lean
|
fix: bitwise shift overflow of UInt types
|
2021-03-17 10:08:02 +01:00 |
|
bitwise.lean.expected.out
|
|
|
|
bool2int.lean
|
|
|
|
bool2int.lean.expected.out
|
|
|
|
bool_simp.lean
|
|
|
|
bool_simp.lean.expected.out
|
|
|
|
bootstrapSorry.lean
|
|
|
|
bootstrapSorry.lean.expected.out
|
chore: improve error message on trying to access an identifier imported privately from the public scope (#10153)
|
2025-08-27 13:43:56 +00:00 |
|
builtinSimprocTrace.lean
|
|
|
|
builtinSimprocTrace.lean.expected.out
|
|
|
|
byCasesMetaM.lean
|
|
|
|
byCasesMetaM.lean.expected.out
|
|
|
|
byStrictIndent.lean
|
|
|
|
byStrictIndent.lean.expected.out
|
|
|
|
bytearray.lean
|
|
|
|
bytearray.lean.expected.out
|
|
|
|
cacheIssue.lean
|
|
|
|
cacheIssue.lean.expected.out
|
|
|
|
calcErrors.lean
|
|
|
|
calcErrors.lean.expected.out
|
|
|
|
casesOnCases.lean
|
|
|
|
casesOnCases.lean.expected.out
|
|
|
|
caseSuggestions.lean
|
|
|
|
caseSuggestions.lean.expected.out
|
|
|
|
cdotTuple.lean
|
chore: style use · instead of . for lambda dot notation
|
2022-03-11 07:49:03 -08:00 |
|
cdotTuple.lean.expected.out
|
feat: cdot notation for tuples
|
2020-12-28 18:08:23 -08:00 |
|
class_def_must_fail.lean
|
|
|
|
class_def_must_fail.lean.expected.out
|
|
|
|
classBadOutParam.lean
|
|
|
|
classBadOutParam.lean.expected.out
|
|
|
|
coe.lean
|
|
|
|
coe.lean.expected.out
|
|
|
|
coeAttr1.lean
|
|
|
|
coeAttr1.lean.expected.out
|
|
|
|
coeM.lean
|
|
|
|
coeM.lean.expected.out
|
|
|
|
collectDepsIssue.lean
|
|
|
|
collectDepsIssue.lean.expected.out
|
|
|
|
commandPrefix.lean
|
feat: in pure code, do use assume Id monad at do notation
|
2021-12-10 12:55:14 -08:00 |
|
commandPrefix.lean.expected.out
|
|
|
|
computedFieldsCode.lean
|
|
|
|
computedFieldsCode.lean.expected.out
|
perf: sort before elim dead branches (#11366)
|
2025-11-27 22:21:06 +00:00 |
|
congrThm.lean
|
|
|
|
congrThm.lean.expected.out
|
|
|
|
congrThmIssue.lean
|
|
|
|
congrThmIssue.lean.expected.out
|
|
|
|
constDelab.lean
|
|
|
|
constDelab.lean.expected.out
|
|
|
|
constructorTac.lean
|
feat: add constructor tactic
|
2021-05-06 10:40:56 -07:00 |
|
constructorTac.lean.expected.out
|
|
|
|
consumePPHint.lean
|
|
|
|
consumePPHint.lean.expected.out
|
|
|
|
conv1.lean
|
|
|
|
conv1.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
convInConv.lean
|
feat: in conv tactic, use try with_reducibe rfl (#3763)
|
2024-03-29 11:59:45 +00:00 |
|
convInConv.lean.expected.out
|
|
|
|
convPatternAtLetIssue.lean
|
feat: optimized simp routine for let telescopes (#8968)
|
2025-06-27 02:13:20 +00:00 |
|
convPatternAtLetIssue.lean.expected.out
|
fix: use consistent goal prefix everywhere
|
2022-05-09 17:49:00 +02:00 |
|
convPatternMatchIssue.lean
|
feat: eliminate letFun support, deprecate let_fun syntax (#9086)
|
2025-06-30 02:10:18 +00:00 |
|
convPatternMatchIssue.lean.expected.out
|
|
|
|
convZetaLetExt.lean
|
|
|
|
convZetaLetExt.lean.expected.out
|
|
|
|
copy-produced
|
|
|
|
csimpAttr.lean
|
|
|
|
csimpAttr.lean.expected.out
|
|
|
|
csimpAttrAppend.lean
|
|
|
|
csimpAttrAppend.lean.expected.out
|
|
|
|
ctor_layout.lean
|
fix: privacy checks and import all (#10550)
|
2025-09-26 13:26:10 +00:00 |
|
ctor_layout.lean.expected.out
|
fix: privacy checks and import all (#10550)
|
2025-09-26 13:26:10 +00:00 |
|
ctorUnivTooBig.lean
|
|
|
|
ctorUnivTooBig.lean.expected.out
|
|
|
|
dbgMacros.lean
|
|
|
|
dbgMacros.lean.expected.out
|
fix: detect private references in inferred type of public def (#10762)
|
2025-10-15 12:51:54 +00:00 |
|
decEqMutualInductives.lean
|
feat: linear-size DecidableEq instance (#10152)
|
2025-09-03 06:31:49 +00:00 |
|
decEqMutualInductives.lean.expected.out
|
refactor: thunk field-less alternatives of casesOnSameCtor (#11254)
|
2025-11-19 09:53:09 +00:00 |
|
decimals.lean
|
|
|
|
decimals.lean.expected.out
|
|
|
|
decreasing_by.lean
|
|
|
|
decreasing_by.lean.expected.out
|
|
|
|
defaultInstance.lean
|
|
|
|
defaultInstance.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
defaultInstanceWithPrio.lean
|
|
|
|
defaultInstanceWithPrio.lean.expected.out
|
|
|
|
defInst.lean
|
|
|
|
defInst.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
delabDoLetFun.lean
|
|
|
|
delabDoLetFun.lean.expected.out
|
|
|
|
delabOverApp.lean
|
|
|
|
delabOverApp.lean.expected.out
|
|
|
|
delabUnexpand.lean
|
|
|
|
delabUnexpand.lean.expected.out
|
|
|
|
delta.lean
|
|
|
|
delta.lean.expected.out
|
|
|
|
deltaRedIndPredBelow.lean
|
|
|
|
deltaRedIndPredBelow.lean.expected.out
|
|
|
|
deprecated.lean
|
fix: generate deprecation warnings for dot notation (#3969)
|
2024-05-09 04:52:09 +00:00 |
|
deprecated.lean.expected.out
|
|
|
|
derivingDecidableEq.lean
|
feat: T.ctor.elim single-constructor cases function (#9952)
|
2025-08-27 09:40:31 +00:00 |
|
derivingDecidableEq.lean.expected.out
|
feat: T.ctor.elim single-constructor cases function (#9952)
|
2025-08-27 09:40:31 +00:00 |
|
derivingHashable.lean
|
|
|
|
derivingHashable.lean.expected.out
|
|
|
|
derivingRpcEncoding.lean
|
feat: reusable rpc refs (#8105)
|
2025-06-03 12:35:12 +00:00 |
|
derivingRpcEncoding.lean.expected.out
|
feat: bundle of widget improvements (#2964)
|
2023-12-21 06:24:33 +00:00 |
|
diamond1.lean
|
|
|
|
diamond1.lean.expected.out
|
|
|
|
diamond2.lean
|
|
|
|
diamond2.lean.expected.out
|
|
|
|
diamond3.lean
|
|
|
|
diamond3.lean.expected.out
|
|
|
|
diamond4.lean
|
|
|
|
diamond4.lean.expected.out
|
|
|
|
diamond5.lean
|
|
|
|
diamond5.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
diamond6.lean
|
|
|
|
diamond6.lean.expected.out
|
|
|
|
diamond7.lean
|
|
|
|
diamond7.lean.expected.out
|
|
|
|
diamond8.lean
|
|
|
|
diamond8.lean.expected.out
|
|
|
|
diamond9.lean
|
|
|
|
diamond9.lean.expected.out
|
|
|
|
diamond10.lean
|
|
|
|
diamond10.lean.expected.out
|
|
|
|
discrTreeIota.lean
|
|
|
|
discrTreeIota.lean.expected.out
|
|
|
|
docStr.lean
|
fix: add_decl_doc should check that declarations are local (#3311)
|
2024-02-12 12:04:51 +00:00 |
|
docStr.lean.expected.out
|
fix: make sure local instance detection sees through reductions (#8903)
|
2025-06-21 06:26:32 +00:00 |
|
docstringLinkValidation.lean
|
|
|
|
docstringLinkValidation.lean.expected.out
|
feat: pre-stage0 groundwork for named error messages (#8649)
|
2025-06-11 14:52:08 +00:00 |
|
doErrorMsg.lean
|
fix: check types at do pattern reassignment
|
2022-06-10 17:31:36 +02:00 |
|
doErrorMsg.lean.expected.out
|
refactor: update built-in tactic error messages (#9633)
|
2025-07-31 14:16:57 +00:00 |
|
doIfLet.lean
|
|
|
|
doIfLet.lean.expected.out
|
|
|
|
doIssue.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
doIssue.lean.expected.out
|
|
|
|
doLetLoop.lean
|
fix: ensure ill-formed if do-statements do not trigger non termination
|
2021-04-13 15:51:20 -07:00 |
|
doLetLoop.lean.expected.out
|
chore: fix tests
|
2022-06-01 06:36:25 -07:00 |
|
doNotation1.lean
|
|
|
|
doNotation1.lean.expected.out
|
|
|
|
doSeqRightIssue.lean
|
|
|
|
doSeqRightIssue.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
doubleReset.lean
|
|
|
|
doubleReset.lean.expected.out
|
perf: sort before elim dead branches (#11366)
|
2025-11-27 22:21:06 +00:00 |
|
dsimpViaConst.lean
|
|
|
|
dsimpViaConst.lean.expected.out
|
|
|
|
dsimpZetaIssue.lean
|
|
|
|
dsimpZetaIssue.lean.expected.out
|
|
|
|
eagerCoeExpansion.lean
|
|
|
|
eagerCoeExpansion.lean.expected.out
|
feat: add option pp.piBinderNames (#10374)
|
2025-09-14 05:15:04 +00:00 |
|
eagerUnfoldingIssue.lean
|
feat: implement MonadLog at CoreM
|
2022-05-31 17:40:55 -07:00 |
|
eagerUnfoldingIssue.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
ellipsisProjIssue.lean
|
fix: disallow . immediately after ..
|
2022-10-26 07:13:40 -07:00 |
|
ellipsisProjIssue.lean.expected.out
|
refactor: replace PRange shape α with Rcc α and eight other types (#10319)
|
2025-10-02 06:45:11 +00:00 |
|
elseifDoErrorPos.lean
|
fix: position information at expandDoIf?
|
2020-12-26 08:26:54 -08:00 |
|
elseifDoErrorPos.lean.expected.out
|
|
|
|
emptyc.lean
|
chore: avoid Has prefix in type classes
|
2020-10-27 18:29:19 -07:00 |
|
emptyc.lean.expected.out
|
|
|
|
emptyTypeAscription.lean
|
feat: empty type ascription syntax (e :) (part 2)
|
2022-11-07 19:10:56 +01:00 |
|
emptyTypeAscription.lean.expected.out
|
|
|
|
eoi.lean
|
|
|
|
eoi.lean.expected.out
|
|
|
|
eraseInsts.lean
|
|
|
|
eraseInsts.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
eraseSimp.lean
|
|
|
|
eraseSimp.lean.expected.out
|
|
|
|
errorOnInductionForNested.lean
|
feat: generate error message when induction tactic is used on a nested inductive type without specifying an eliminator
|
2022-03-11 14:45:57 -08:00 |
|
errorOnInductionForNested.lean.expected.out
|
refactor: update built-in tactic error messages (#9633)
|
2025-07-31 14:16:57 +00:00 |
|
errorRecoveryBug.lean
|
|
|
|
errorRecoveryBug.lean.expected.out
|
fix: antipattern
|
2021-04-07 10:26:05 -07:00 |
|
eta.lean
|
|
|
|
eta.lean.expected.out
|
|
|
|
etaReducedMvarAssignments.lean
|
|
|
|
etaReducedMvarAssignments.lean.expected.out
|
|
|
|
etaStructIssue.lean
|
|
|
|
etaStructIssue.lean.expected.out
|
|
|
|
eval_except.lean
|
|
|
|
eval_except.lean.expected.out
|
|
|
|
evalCmd.lean
|
feat: add support for CommandElabM at #eval
|
2022-06-29 16:34:49 -07:00 |
|
evalCmd.lean.expected.out
|
|
|
|
evalInstMessage.lean
|
feat: improve error message produced by #eval command when it fails to synthesize "eval" instance
|
2021-11-05 15:03:57 -07:00 |
|
evalInstMessage.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
evalLeak.lean
|
|
|
|
evalLeak.lean.expected.out
|
|
|
|
evalNone.lean
|
|
|
|
evalNone.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
evalSorry.lean
|
fix: do not evaluate code containing sorry
|
2021-01-26 15:01:53 -08:00 |
|
evalSorry.lean.expected.out
|
|
|
|
evalWithMVar.lean
|
chore: remove new_frontend from tests
|
2020-10-25 09:16:38 -07:00 |
|
evalWithMVar.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
exactErrorPos.lean
|
|
|
|
exactErrorPos.lean.expected.out
|
|
|
|
exceptionalTrace.lean
|
|
|
|
exceptionalTrace.lean.expected.out
|
|
|
|
exitAfterParseError.lean
|
|
|
|
exitAfterParseError.lean.expected.out
|
|
|
|
expandExplicitBinders.lean
|
|
|
|
expandExplicitBinders.lean.expected.out
|
|
|
|
externBoxing.lean
|
fix: miscompilation resulting in minor memory leak on extern projections with unboxed arguments (#11383)
|
2025-11-26 19:27:43 +00:00 |
|
externBoxing.lean.expected.out
|
fix: miscompilation resulting in minor memory leak on extern projections with unboxed arguments (#11383)
|
2025-11-26 19:27:43 +00:00 |
|
extract.lean
|
|
|
|
extract.lean.expected.out
|
|
|
|
failTac.lean
|
|
|
|
failTac.lean.expected.out
|
|
|
|
file_not_found.lean
|
|
|
|
file_not_found.lean.expected.out
|
|
|
|
filePath.lean
|
|
|
|
filePath.lean.expected.out
|
|
|
|
fixedIndexToParamIssue.lean
|
|
|
|
fixedIndexToParamIssue.lean.expected.out
|
feat: enable pp.fieldNotation.generalized globally (#3744)
|
2024-03-23 02:38:09 +00:00 |
|
fixedIndicesToParams.lean
|
|
|
|
fixedIndicesToParams.lean.expected.out
|
|
|
|
forallMetaBounded.lean
|
|
|
|
forallMetaBounded.lean.expected.out
|
|
|
|
forErrors.lean
|
|
|
|
forErrors.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
Format.lean
|
chore: remove remaining #lang lean4 in tests
|
2021-01-27 14:45:31 +01:00 |
|
Format.lean.expected.out
|
feat: Format.fill
|
2020-10-07 15:30:36 +02:00 |
|
formatTerm.lean
|
|
|
|
formatTerm.lean.expected.out
|
fix: trailing whitespace in location formatter (#3318)
|
2024-02-13 15:53:29 +00:00 |
|
fun.lean
|
refactor: avoid nested sequence in simpleBinder
|
2022-07-08 19:06:10 +02:00 |
|
fun.lean.expected.out
|
|
|
|
funExpected.lean
|
|
|
|
funExpected.lean.expected.out
|
|
|
|
funind_errors.lean
|
chore: remove >6 month old deprecations (#10446)
|
2025-09-22 12:47:11 +00:00 |
|
funind_errors.lean.expected.out
|
fix: deprecation warning location with field notation (#10826)
|
2025-10-23 20:55:25 +00:00 |
|
funind_reserved.lean
|
|
|
|
funind_reserved.lean.expected.out
|
|
|
|
funInfoBug.lean
|
|
|
|
funInfoBug.lean.expected.out
|
|
|
|
funParen.lean
|
|
|
|
funParen.lean.expected.out
|
|
|
|
gcd.lean
|
feat: add Nat.gcd
|
2021-03-07 18:47:02 -08:00 |
|
gcd.lean.expected.out
|
|
|
|
getElem.lean
|
|
|
|
getElem.lean.expected.out
|
|
|
|
guessLex.lean
|
|
|
|
guessLex.lean.expected.out
|
|
|
|
guessLexDiff.lean
|
feat: always run clean_wf, even before decreasing_by (#5016)
|
2024-08-15 14:42:15 +00:00 |
|
guessLexDiff.lean.expected.out
|
|
|
|
guessLexFailures.lean
|
|
|
|
guessLexFailures.lean.expected.out
|
fix: decreasing_by: preserve variable names of match alts (#10980)
|
2025-10-27 14:00:36 +00:00 |
|
guessLexTricky.lean
|
|
|
|
guessLexTricky.lean.expected.out
|
|
|
|
guessLexTricky2.lean
|
|
|
|
guessLexTricky2.lean.expected.out
|
|
|
|
have.lean
|
|
|
|
have.lean.expected.out
|
|
|
|
hidingInaccessibleNames.lean
|
|
|
|
hidingInaccessibleNames.lean.expected.out
|
|
|
|
holeErrors.lean
|
|
|
|
holeErrors.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
holes.lean
|
|
|
|
holes.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
hpow.lean
|
feat: upstream several Rat lemmas from mathlib (#10077)
|
2025-08-25 06:02:27 +00:00 |
|
hpow.lean.expected.out
|
|
|
|
hygienicIntro.lean
|
|
|
|
hygienicIntro.lean.expected.out
|
|
|
|
implementedByIssue.lean
|
|
|
|
implementedByIssue.lean.expected.out
|
chore: use ofConstName in error messages (#10121)
|
2025-08-25 23:20:36 +00:00 |
|
implicitArgumentError.lean
|
|
|
|
implicitArgumentError.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
implicitLambdaIssue.lean
|
|
|
|
implicitLambdaIssue.lean.expected.out
|
test: add Kevin and Yakov's examples
|
2021-03-25 17:22:14 -07:00 |
|
implicitTypePos.lean
|
fix: position information for implicit type
|
2021-08-26 08:07:16 -07:00 |
|
implicitTypePos.lean.expected.out
|
feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)
|
2025-07-18 19:20:31 +00:00 |
|
indimpltarget.lean
|
|
|
|
indimpltarget.lean.expected.out
|
refactor: update built-in tactic error messages (#9633)
|
2025-07-31 14:16:57 +00:00 |
|
inductionErrors.lean
|
|
|
|
inductionErrors.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
inductionGen.lean
|
fix: checkTargets check for duplicate target (#3171)
|
2024-01-18 09:44:17 +00:00 |
|
inductionGen.lean.expected.out
|
|
|
|
inductionMutual.lean
|
|
|
|
inductionMutual.lean.expected.out
|
|
|
|
inductionParse.lean
|
|
|
|
inductionParse.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
inductive1.lean
|
|
|
|
inductive1.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
inductiveUnivErrorMsg.lean
|
feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures
|
2022-05-10 18:30:53 -07:00 |
|
inductiveUnivErrorMsg.lean.expected.out
|
|
|
|
indUsingTerm.lean
|
chore: fix spelling mistakes in tests (#5439)
|
2024-09-24 03:22:53 +00:00 |
|
indUsingTerm.lean.expected.out
|
feat: induction using <term> (#3188)
|
2024-01-25 16:57:41 +00:00 |
|
inlineIssue.lean
|
|
|
|
inlineIssue.lean.expected.out
|
feat: better #eval command (#5627)
|
2024-10-08 20:51:46 +00:00 |
|
inst.lean
|
|
|
|
inst.lean.expected.out
|
|
|
|
instance1.lean
|
chore: add test
|
2022-09-13 06:19:40 -07:00 |
|
instance1.lean.expected.out
|
|
|
|
int_div_mod.lean
|
|
|
|
int_div_mod.lean.expected.out
|
|
|
|
intModBug.lean
|
test: test for Int.mod bug
|
2021-01-31 08:57:41 -08:00 |
|
intModBug.lean.expected.out
|
|
|
|
intNegSucc.lean
|
|
|
|
intNegSucc.lean.expected.out
|
|
|
|
introLetBug.lean
|
|
|
|
introLetBug.lean.expected.out
|
|
|
|
invalidFieldName.lean
|
|
|
|
invalidFieldName.lean.expected.out
|
|
|
|
invalidInstImplicit.lean
|
|
|
|
invalidInstImplicit.lean.expected.out
|
|
|
|
invalidMutualError.lean
|
feat: detail error message about invalid mutual blocks (#2949)
|
2023-12-05 10:50:10 +00:00 |
|
invalidMutualError.lean.expected.out
|
feat: allow structure in mutual blocks (#6125)
|
2024-11-22 09:20:07 +00:00 |
|
invalidNamedArgs.lean
|
|
|
|
invalidNamedArgs.lean.expected.out
|
|
|
|
invalidPatternIssue.lean
|
fix: ensure explicit pattern variables provided by the uses are indeed pattern variables
|
2022-03-16 07:50:29 -07:00 |
|
invalidPatternIssue.lean.expected.out
|
|
|
|
IRbug.lean
|
feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)
|
2024-11-22 03:05:51 +00:00 |
|
IRbug.lean.expected.out
|
|
|
|
isDefEqOffsetBug.lean
|
|
|
|
isDefEqOffsetBug.lean.expected.out
|
|
|
|
isNoncomputable.lean
|
|
|
|
isNoncomputable.lean.expected.out
|
|
|
|
issue2260.lean
|
|
|
|
issue2260.lean.expected.out
|
|
|
|
issue2981.lean
|
|
|
|
issue2981.lean.expected.out
|
|
|
|
issue3232.lean
|
feat: consider universes and projections in addPPExplicitToExposeDiff (#8271)
|
2025-05-09 15:07:50 +00:00 |
|
issue3232.lean.expected.out
|
|
|
|
jason2.lean
|
|
|
|
jason2.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
jpCasesDiscrM.lean
|
|
|
|
jpCasesDiscrM.lean.expected.out
|
|
|
|
jpCasesNary.lean
|
|
|
|
jpCasesNary.lean.expected.out
|
|
|
|
jpClosureIssue.lean
|
|
|
|
jpClosureIssue.lean.expected.out
|
feat: zero cost BaseIO (#10625)
|
2025-10-22 10:55:12 +02:00 |
|
json.lean
|
feat: fromJson? derivations now say where a parsing error occurred (#1656)
|
2022-09-28 09:15:26 +00:00 |
|
json.lean.expected.out
|
feat: fromJson? derivations now say where a parsing error occurred (#1656)
|
2022-09-28 09:15:26 +00:00 |
|
kernelMVarBug.lean
|
|
|
|
kernelMVarBug.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
keyAttrErase.lean
|
|
|
|
keyAttrErase.lean.expected.out
|
|
|
|
lambdaLiftCache.lean
|
chore: reenable subset of new-compiler tests and delete others
|
2025-06-20 17:29:10 +02:00 |
|
lambdaLiftCache.lean.expected.out
|
|
|
|
lazySeq.lean
|
|
|
|
lazySeq.lean.expected.out
|
|
|
|
lcnfTypes.lean
|
|
|
|
lcnfTypes.lean.expected.out
|
feat: zero cost BaseIO (#10625)
|
2025-10-22 10:55:12 +02:00 |
|
LE.lean
|
feat: make #check <ident> always show the signature without elaboration
|
2022-12-21 21:59:05 +01:00 |
|
LE.lean.expected.out
|
|
|
|
lean3RefineBug.lean
|
|
|
|
lean3RefineBug.lean.expected.out
|
|
|
|
letArrowOutsideDo.lean
|
|
|
|
letArrowOutsideDo.lean.expected.out
|
|
|
|
letFun.lean
|
feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)
|
2025-06-22 21:54:57 +00:00 |
|
letFun.lean.expected.out
|
|
|
|
letPatIssue.lean
|
feat: improve let-pattern and have-pattern macro expansion
|
2022-03-29 07:33:22 -07:00 |
|
letPatIssue.lean.expected.out
|
|
|
|
letrec1.lean
|
|
|
|
letrec1.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
letrecErrors.lean
|
|
|
|
letrecErrors.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
letRecTheorem.lean
|
feat: infer def/theorem DefKind for let rec
|
2022-11-29 08:16:47 -08:00 |
|
letRecTheorem.lean.expected.out
|
|
|
|
librarySearch.lean
|
feat: "try this" messages with support for interactivity (#10524)
|
2025-10-13 13:39:03 +00:00 |
|
librarySearch.lean.expected.out
|
feat: "try this" messages with support for interactivity (#10524)
|
2025-10-13 13:39:03 +00:00 |
|
liftOverLeft.lean
|
|
|
|
liftOverLeft.lean.expected.out
|
|
|
|
linterMissingDocs.lean
|
|
|
|
linterMissingDocs.lean.expected.out
|
|
|
|
linterSuspiciousUnexpanderPatterns.lean
|
|
|
|
linterSuspiciousUnexpanderPatterns.lean.expected.out
|
|
|
|
linterUnusedVariables.lean
|
|
|
|
linterUnusedVariables.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
listLength.lean
|
|
|
|
listLength.lean.expected.out
|
|
|
|
lit_values.lean
|
|
|
|
lit_values.lean.expected.out
|
|
|
|
localNotationPP.lean
|
|
|
|
localNotationPP.lean.expected.out
|
|
|
|
longestParsePrio.lean
|
|
|
|
longestParsePrio.lean.expected.out
|
|
|
|
loopErrorRecovery.lean
|
fix: loop due to error recovery
|
2021-04-13 08:12:39 -07:00 |
|
loopErrorRecovery.lean.expected.out
|
|
|
|
lvl1.lean
|
|
|
|
lvl1.lean.expected.out
|
|
|
|
macroElabRulesIssue1.lean
|
fix: evalTactic
|
2022-07-19 23:28:14 -04:00 |
|
macroElabRulesIssue1.lean.expected.out
|
|
|
|
macroElabRulesIssue2.lean
|
|
|
|
macroElabRulesIssue2.lean.expected.out
|
|
|
|
macroError.lean
|
fix: term macro errors should be fatal
|
2022-01-04 11:20:18 +01:00 |
|
macroError.lean.expected.out
|
fix: term macro errors should be fatal
|
2022-01-04 11:20:18 +01:00 |
|
macroPrio.lean
|
|
|
|
macroPrio.lean.expected.out
|
|
|
|
macroResolveName.lean
|
|
|
|
macroResolveName.lean.expected.out
|
|
|
|
macroscopes.lean
|
perf: make macro scope numbering less dependent on surrounding context (#10027)
|
2025-08-22 13:16:02 +00:00 |
|
macroscopes.lean.expected.out
|
|
|
|
macroStack.lean
|
|
|
|
macroStack.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
macroSwizzle.lean
|
|
|
|
macroSwizzle.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
macroTrace.lean
|
|
|
|
macroTrace.lean.expected.out
|
|
|
|
mangling.lean.expected.out
|
|
|
|
match2.lean
|
|
|
|
match2.lean.expected.out
|
|
|
|
match3.lean
|
|
|
|
match3.lean.expected.out
|
|
|
|
match4.lean
|
chore: remove >6 month old deprecations (#10968)
|
2025-10-26 10:01:30 +00:00 |
|
match4.lean.expected.out
|
|
|
|
matchAltIndent.lean
|
|
|
|
matchAltIndent.lean.expected.out
|
|
|
|
matchApp.lean
|
|
|
|
matchApp.lean.expected.out
|
|
|
|
matchErrorLocation.lean
|
|
|
|
matchErrorLocation.lean.expected.out
|
|
|
|
matchErrorMsg.lean
|
feat: improve match error message
|
2021-01-14 14:58:34 -08:00 |
|
matchErrorMsg.lean.expected.out
|
feat: improve error messages in invalid match alternatives (#8368)
|
2025-05-19 17:40:41 +00:00 |
|
matchLeftovers.lean
|
|
|
|
matchLeftovers.lean.expected.out
|
|
|
|
matchMissingCasesAsStuckError.lean
|
|
|
|
matchMissingCasesAsStuckError.lean.expected.out
|
|
|
|
matchMultAlt.lean
|
|
|
|
matchMultAlt.lean.expected.out
|
|
|
|
matchOfNatIssue.lean
|
|
|
|
matchOfNatIssue.lean.expected.out
|
|
|
|
matchOrIssue.lean
|
|
|
|
matchOrIssue.lean.expected.out
|
|
|
|
matchPatternInsideBinders.lean
|
|
|
|
matchPatternInsideBinders.lean.expected.out
|
|
|
|
matchPatternPartialApp.lean
|
feat: in conv tactic, use try with_reducibe rfl (#3763)
|
2024-03-29 11:59:45 +00:00 |
|
matchPatternPartialApp.lean.expected.out
|
fix: use consistent goal prefix everywhere
|
2022-05-09 17:49:00 +02:00 |
|
matchunit.lean
|
|
|
|
matchunit.lean.expected.out
|
|
|
|
matchUnknownFVarBug.lean
|
|
|
|
matchUnknownFVarBug.lean.expected.out
|
|
|
|
matchVarNames.lean
|
|
|
|
matchVarNames.lean.expected.out
|
|
|
|
metaEvalInstMessage.lean
|
|
|
|
metaEvalInstMessage.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
modBug.lean
|
|
|
|
modBug.lean.expected.out
|
|
|
|
moduleDoc.lean
|
feat: add position to mod doc
|
2022-02-16 13:50:19 -08:00 |
|
moduleDoc.lean.expected.out
|
|
|
|
moduleKeywords.lean
|
|
|
|
moduleKeywords.lean.expected.out
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
moduleOf.lean
|
chore: remove the old Lean.Data.HashMap implementation (#7519)
|
2025-03-20 23:49:55 +00:00 |
|
moduleOf.lean.expected.out
|
feat: docstrings with Verso syntax (#10307)
|
2025-09-10 07:03:57 +00:00 |
|
motiveNotTypeCorrect.lean
|
chore: fix spelling errors (#10042)
|
2025-08-22 07:23:12 +00:00 |
|
motiveNotTypeCorrect.lean.expected.out
|
chore: fix spelling errors (#10042)
|
2025-08-22 07:23:12 +00:00 |
|
mulcommErrorMessage.lean
|
feat: improve error message and include variables introduced by the implicit lambda notation
|
2021-04-24 21:34:42 -07:00 |
|
mulcommErrorMessage.lean.expected.out
|
refactor: update built-in tactic error messages (#9633)
|
2025-07-31 14:16:57 +00:00 |
|
multiConstantError.lean
|
chore: fix tests
|
2022-06-14 16:43:22 -07:00 |
|
multiConstantError.lean.expected.out
|
feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)
|
2025-07-18 19:20:31 +00:00 |
|
mutualdef1.lean
|
|
|
|
mutualdef1.lean.expected.out
|
|
|
|
mutualWithNamespaceMacro.lean
|
feat: multiple namespaces in mutual declarations
|
2022-08-04 19:18:49 -07:00 |
|
mutualWithNamespaceMacro.lean.expected.out
|
|
|
|
mutwf1.lean
|
|
|
|
mutwf1.lean.expected.out
|
|
|
|
mutwftypemismatch.lean
|
|
|
|
mutwftypemismatch.lean.expected.out
|
|
|
|
mvar_fvar.lean
|
|
|
|
mvar_fvar.lean.expected.out
|
|
|
|
mvarAtDefaultValue.lean
|
fix: throw error when default value contains metavariables
|
2021-02-20 11:31:56 -08:00 |
|
mvarAtDefaultValue.lean.expected.out
|
|
|
|
nameArgErrorIssue.lean
|
feat: improve argument type mismatch error position, and do not stop at application type mismatch errors
|
2022-04-25 16:30:40 -07:00 |
|
nameArgErrorIssue.lean.expected.out
|
feat: add named argument hints (#9315)
|
2025-07-17 03:22:25 +00:00 |
|
namedHoles.lean
|
|
|
|
namedHoles.lean.expected.out
|
|
|
|
namelit.lean
|
|
|
|
namelit.lean.expected.out
|
|
|
|
nameRepr.lean
|
|
|
|
nameRepr.lean.expected.out
|
|
|
|
negFloat.lean
|
|
|
|
negFloat.lean.expected.out
|
|
|
|
newCatPanic.lean
|
|
|
|
newCatPanic.lean.expected.out
|
|
|
|
nonAtomicFieldName.lean
|
|
|
|
nonAtomicFieldName.lean.expected.out
|
|
|
|
noncompSection.lean
|
|
|
|
noncompSection.lean.expected.out
|
feat: add initial error explanations (#8934)
|
2025-06-23 17:24:09 +00:00 |
|
nondepArrow.lean
|
|
|
|
nondepArrow.lean.expected.out
|
|
|
|
nonfatalattrs.lean
|
|
|
|
nonfatalattrs.lean.expected.out
|
|
|
|
nonReserved.lean
|
|
|
|
nonReserved.lean.expected.out
|
|
|
|
noTabs.lean
|
|
|
|
noTabs.lean.expected.out
|
|
|
|
notationDelab.lean
|
|
|
|
notationDelab.lean.expected.out
|
|
|
|
notationPrecheck.lean
|
feat: quotation precheck for choice nodes
|
2022-03-29 10:50:11 +02:00 |
|
notationPrecheck.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
notNaturalNumbersGame.lean
|
feat: catch and provide context for misuse of NNG-style induction pattern (#11347)
|
2025-11-25 18:44:40 +00:00 |
|
notNaturalNumbersGame.lean.expected.out
|
feat: catch and provide context for misuse of NNG-style induction pattern (#11347)
|
2025-11-25 18:44:40 +00:00 |
|
openExport.lean
|
|
|
|
openExport.lean.expected.out
|
|
|
|
openScoped.lean
|
|
|
|
openScoped.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
optionGetD.lean
|
|
|
|
optionGetD.lean.expected.out
|
|
|
|
or_shortcircuit.lean
|
|
|
|
or_shortcircuit.lean.expected.out
|
|
|
|
parserPrio.lean
|
chore: two comments about bad pp.analyze behavior
|
2021-08-03 09:13:18 +02:00 |
|
parserPrio.lean.expected.out
|
feat: improve projection and field-notation errors (#8986)
|
2025-06-26 18:36:47 +00:00 |
|
parserRecovery.lean
|
feat: custom error recovery in parser (#3413)
|
2024-02-21 14:29:54 +00:00 |
|
parserRecovery.lean.expected.out
|
feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)
|
2025-07-18 19:20:31 +00:00 |
|
partial_fixpoint_parseerrors.lean
|
feat: partial_fixpoint: partial functions with equations (#6355)
|
2025-01-21 09:54:30 +00:00 |
|
partial_fixpoint_parseerrors.lean.expected.out
|
feat: partial_fixpoint: partial functions with equations (#6355)
|
2025-01-21 09:54:30 +00:00 |
|
partialIssue.lean
|
|
|
|
partialIssue.lean.expected.out
|
|
|
|
partialSyntaxTraces.lean
|
feat: snapshot trees and language processors (#3014)
|
2024-03-14 13:40:08 +00:00 |
|
partialSyntaxTraces.lean.expected.out
|
|
|
|
partialVariable.lean
|
|
|
|
partialVariable.lean.expected.out
|
feat: include unexpected token in error message
|
2023-09-12 11:42:24 +02:00 |
|
patvar.lean
|
|
|
|
patvar.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
phashmap_inst_coherence.lean
|
|
|
|
phashmap_inst_coherence.lean.expected.out
|
|
|
|
ppBeta.lean
|
|
|
|
ppBeta.lean.expected.out
|
|
|
|
ppDeepTerms.lean
|
fix: make omission syntax be a builtin syntax (part 2)
|
2024-02-28 09:23:17 +01:00 |
|
ppDeepTerms.lean.expected.out
|
|
|
|
ppExpr.lean
|
chore: remove unnecessary args
|
2022-04-07 18:19:15 -07:00 |
|
ppExpr.lean.expected.out
|
|
|
|
PPInstances.lean
|
|
|
|
PPInstances.lean.expected.out
|
|
|
|
ppite.lean
|
|
|
|
ppite.lean.expected.out
|
|
|
|
pplevel.lean
|
|
|
|
pplevel.lean.expected.out
|
|
|
|
ppMotives.lean
|
|
|
|
ppMotives.lean.expected.out
|
|
|
|
ppNotationCode.lean
|
|
|
|
ppNotationCode.lean.expected.out
|
chore: rename Substring to Substring.Raw (#11154)
|
2025-11-16 09:30:04 +00:00 |
|
ppProofs.lean
|
feat: have pp.proofs use ⋯ for omission (#3241)
|
2024-02-15 21:49:41 +00:00 |
|
ppProofs.lean.expected.out
|
|
|
|
PPRoundtrip.lean
|
|
|
|
PPRoundtrip.lean.expected.out
|
|
|
|
ppSyntax.lean
|
feat: strengthen pp* signatures
|
2022-07-03 19:14:49 +02:00 |
|
ppSyntax.lean.expected.out
|
fix: fix pretty printers for imported ParserDescrs
|
2020-11-07 17:05:07 +01:00 |
|
precissues.lean
|
|
|
|
precissues.lean.expected.out
|
|
|
|
private.lean
|
|
|
|
private.lean.expected.out
|
fix: pretty print dot notation for private definitions on public types (#10122)
|
2025-08-27 03:30:52 +00:00 |
|
privateFieldCopyIssue.lean
|
fix: propagate visibility annotation
|
2021-08-10 15:34:07 -07:00 |
|
privateFieldCopyIssue.lean.expected.out
|
|
|
|
Process.lean
|
test: remove flaky test (#5468)
|
2024-09-25 08:18:42 +00:00 |
|
Process.lean.expected.out
|
test: remove flaky test (#5468)
|
2024-09-25 08:18:42 +00:00 |
|
promise.lean
|
|
|
|
promise.lean.expected.out
|
|
|
|
protected.lean
|
feat: subsume variables under variable
|
2021-01-22 14:36:05 +01:00 |
|
protected.lean.expected.out
|
|
|
|
protectedAlias.lean
|
|
|
|
protectedAlias.lean.expected.out
|
|
|
|
pureCoeIssue.lean
|
|
|
|
pureCoeIssue.lean.expected.out
|
|
|
|
rat1.lean
|
feat: upstream definition of Rat from Batteries (#9957)
|
2025-08-19 01:58:24 +00:00 |
|
rat1.lean.expected.out
|
|
|
|
rawStringEOF.lean
|
feat: Rust-style raw string literals (#2929)
|
2023-12-20 16:53:08 +00:00 |
|
rawStringEOF.lean.expected.out
|
feat: Rust-style raw string literals (#2929)
|
2023-12-20 16:53:08 +00:00 |
|
readDir.lean
|
feat: make FilePath a concrete type
|
2021-05-28 14:19:59 +02:00 |
|
readDir.lean.expected.out
|
|
|
|
reduceArity.lean
|
|
|
|
reduceArity.lean.expected.out
|
perf: sort before elim dead branches (#11366)
|
2025-11-27 22:21:06 +00:00 |
|
reduceBool.lean
|
|
|
|
reduceBool.lean.expected.out
|
|
|
|
redundantAlt.lean
|
|
|
|
redundantAlt.lean.expected.out
|
fix: preserve error locations when expanding match arms (#10783)
|
2025-10-15 13:31:42 +00:00 |
|
ref1.lean
|
chore: remove >6 month old deprecations (#10446)
|
2025-09-22 12:47:11 +00:00 |
|
ref1.lean.expected.out
|
|
|
|
refineFiltersOldMVars.lean
|
|
|
|
refineFiltersOldMVars.lean.expected.out
|
|
|
|
refineOccursCheck.lean
|
|
|
|
refineOccursCheck.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
Reformat.lean
|
fix: apply newlines before and after comments when formatting syntax (#8626)
|
2025-06-26 19:23:35 +00:00 |
|
Reformat.lean.expected.out
|
|
|
|
renameBug.lean
|
|
|
|
renameBug.lean.expected.out
|
|
|
|
renameI.lean
|
|
|
|
renameI.lean.expected.out
|
|
|
|
replaceLocalDeclInstantiateMVars.lean
|
fix: add instantiateMVars to replaceLocalDecl (#2712)
|
2023-10-25 10:26:09 +11:00 |
|
replaceLocalDeclInstantiateMVars.lean.expected.out
|
|
|
|
repr.lean
|
|
|
|
repr.lean.expected.out
|
|
|
|
repr_issue.lean
|
chore: remove >6 month old deprecations (#10968)
|
2025-10-26 10:01:30 +00:00 |
|
repr_issue.lean.expected.out
|
|
|
|
resolveGlobalName.lean
|
|
|
|
resolveGlobalName.lean.expected.out
|
|
|
|
revertlet.lean
|
|
|
|
revertlet.lean.expected.out
|
|
|
|
rewrite.lean
|
|
|
|
rewrite.lean.expected.out
|
|
|
|
rfl_simp_thm.lean
|
|
|
|
rfl_simp_thm.lean.expected.out
|
|
|
|
root.lean
|
|
|
|
root.lean.expected.out
|
fix: detect private references in inferred type of public def (#10762)
|
2025-10-15 12:51:54 +00:00 |
|
run_meta1.lean
|
|
|
|
run_meta1.lean.expected.out
|
|
|
|
runSTBug.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
runSTBug.lean.expected.out
|
|
|
|
runTacticMustCatchExceptions.lean
|
feat: improve runTactic
|
2022-07-25 07:41:50 -07:00 |
|
runTacticMustCatchExceptions.lean.expected.out
|
|
|
|
rwEqThms.lean
|
|
|
|
rwEqThms.lean.expected.out
|
|
|
|
rwPrioritizesLCtxOverEnv.lean
|
|
|
|
rwPrioritizesLCtxOverEnv.lean.expected.out
|
|
|
|
rwWithoutOffsetCnstrs.lean
|
|
|
|
rwWithoutOffsetCnstrs.lean.expected.out
|
|
|
|
rwWithSynthesizeBug.lean
|
|
|
|
rwWithSynthesizeBug.lean.expected.out
|
|
|
|
sanitizeMacroScopes.lean
|
|
|
|
sanitizeMacroScopes.lean.expected.out
|
|
|
|
sanitychecks.lean
|
|
|
|
sanitychecks.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
scientific.lean
|
|
|
|
scientific.lean.expected.out
|
|
|
|
scopedInstanceOutsideNamespace.lean
|
|
|
|
scopedInstanceOutsideNamespace.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
scopedLocalInsts.lean
|
|
|
|
scopedLocalInsts.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
scopedMacros.lean
|
|
|
|
scopedMacros.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
scopedTokens.lean
|
|
|
|
scopedTokens.lean.expected.out
|
|
|
|
scopedunifhint.lean.expected.out
|
|
|
|
semicolonOrLinebreak.lean
|
|
|
|
semicolonOrLinebreak.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
sepByIndentQuot.lean
|
|
|
|
sepByIndentQuot.lean.expected.out
|
|
|
|
seqToCodeIssue.lean
|
chore: reenable subset of new-compiler tests and delete others
|
2025-06-20 17:29:10 +02:00 |
|
seqToCodeIssue.lean.expected.out
|
feat: zero cost BaseIO (#10625)
|
2025-10-22 10:55:12 +02:00 |
|
setLit.lean
|
|
|
|
setLit.lean.expected.out
|
refactor: rename String.bytes to String.toByteArray (#11343)
|
2025-11-24 18:59:49 +00:00 |
|
shadow.lean
|
|
|
|
shadow.lean.expected.out
|
perf: make macro scope numbering less dependent on surrounding context (#10027)
|
2025-08-22 13:16:02 +00:00 |
|
simp_all_duplicateHyps.lean
|
|
|
|
simp_all_duplicateHyps.lean.expected.out
|
|
|
|
simp_dsimp.lean
|
|
|
|
simp_dsimp.lean.expected.out
|
|
|
|
simp_trace.lean
|
|
|
|
simp_trace.lean.expected.out
|
|
|
|
simp_trace_backtrack.lean
|
|
|
|
simp_trace_backtrack.lean.expected.out
|
|
|
|
simpArgTypeMismatch.lean
|
|
|
|
simpArgTypeMismatch.lean.expected.out
|
|
|
|
simpArrayIdx.lean
|
chore: deprecate Array.get
|
2025-02-19 08:48:33 +11:00 |
|
simpArrayIdx.lean.expected.out
|
feat: port check_tactic commands from Std and add test cases (#3532)
|
2024-02-28 23:32:54 +00:00 |
|
simpcfg.lean
|
|
|
|
simpcfg.lean.expected.out
|
|
|
|
simpDisch.lean
|
|
|
|
simpDisch.lean.expected.out
|
|
|
|
simpPrefixIssue.lean
|
|
|
|
simpPrefixIssue.lean.expected.out
|
|
|
|
simprocChar.lean
|
|
|
|
simprocChar.lean.expected.out
|
|
|
|
simprocEval1.lean
|
|
|
|
simprocEval1.lean.expected.out
|
|
|
|
simprocEval2.lean
|
|
|
|
simprocEval2.lean.expected.out
|
|
|
|
simprocEval3.lean
|
|
|
|
simprocEval3.lean.expected.out
|
|
|
|
simprocEval4.lean
|
chore: simprocs for Eq
|
2024-02-17 17:51:24 -08:00 |
|
simprocEval4.lean.expected.out
|
|
|
|
simprocTrace.lean
|
|
|
|
simprocTrace.lean.expected.out
|
|
|
|
simpTracePostIssue.lean
|
|
|
|
simpTracePostIssue.lean.expected.out
|
|
|
|
simpZetaFalse.lean
|
|
|
|
simpZetaFalse.lean.expected.out
|
|
|
|
sint_basic.lean
|
fix: expose Int* definitions for simprocs and decide (fixes #10546) (#10631)
|
2025-10-01 15:53:02 +00:00 |
|
sint_basic.lean.expected.out
|
fix: detect private references in inferred type of public def (#10762)
|
2025-10-15 12:51:54 +00:00 |
|
sizeof.lean
|
|
|
|
sizeof.lean.expected.out
|
feat: redefine String, part one (#10304)
|
2025-09-18 11:36:52 +00:00 |
|
smartUnfolding.lean
|
|
|
|
smartUnfolding.lean.expected.out
|
|
|
|
smartUnfoldingMatch.lean
|
|
|
|
smartUnfoldingMatch.lean.expected.out
|
|
|
|
sorryAtError.lean
|
|
|
|
sorryAtError.lean.expected.out
|
|
|
|
sorryWarning.lean
|
|
|
|
sorryWarning.lean.expected.out
|
|
|
|
specializeAttr.lean
|
|
|
|
specializeAttr.lean.expected.out
|
|
|
|
split_mvars_target.lean
|
|
|
|
split_mvars_target.lean.expected.out
|
|
|
|
splitIssue.lean
|
chore: simp_arith has been deprecated (#7043)
|
2025-02-12 03:55:45 +00:00 |
|
splitIssue.lean.expected.out
|
|
|
|
stdio.lean
|
|
|
|
stdio.lean.expected.out
|
|
|
|
stream.lean
|
chore: rename Stream to Std.Stream (#10645)
|
2025-10-02 15:25:56 +00:00 |
|
stream.lean.expected.out
|
|
|
|
strictImplicit.lean
|
|
|
|
strictImplicit.lean.expected.out
|
|
|
|
string_gaps_err_newline.lean
|
|
|
|
string_gaps_err_newline.lean.expected.out
|
|
|
|
string_imp.lean
|
fix: String.splitOn bug (#3832)
|
2024-04-04 09:30:53 +00:00 |
|
string_imp.lean.expected.out
|
fix: String.splitOn bug (#3832)
|
2024-04-04 09:30:53 +00:00 |
|
string_imp2.lean
|
refactor: use String.Slice in String.take and variants (#11180)
|
2025-11-18 16:13:48 +00:00 |
|
string_imp2.lean.expected.out
|
chore: rename Substring to Substring.Raw (#11154)
|
2025-11-16 09:30:04 +00:00 |
|
struct1.lean
|
|
|
|
struct1.lean.expected.out
|
|
|
|
structAutoBound.lean
|
|
|
|
structAutoBound.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
structDefault.lean
|
test: add structure field default value test
|
2020-12-23 08:35:27 -08:00 |
|
structDefault.lean.expected.out
|
refactor: update built-in tactic error messages (#9633)
|
2025-07-31 14:16:57 +00:00 |
|
structDefValueOverride.lean
|
|
|
|
structDefValueOverride.lean.expected.out
|
feat: update structure/inductive error messages (#9592)
|
2025-07-29 21:27:30 +00:00 |
|
structInst1.lean
|
feat: allow multiple source + no expected type
|
2022-09-13 07:09:08 -07:00 |
|
structInst1.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
structInstError.lean
|
feat: improve {...} error message
|
2020-12-24 09:35:55 -08:00 |
|
structInstError.lean.expected.out
|
feat: pp.analyze detect when struct-inst type needed
|
2021-08-03 09:13:18 +02:00 |
|
structInstSourcesLeftToRight.lean
|
feat: flatten parent projections when pretty printing structure instance notation (#3749)
|
2024-03-23 09:20:52 +00:00 |
|
structInstSourcesLeftToRight.lean.expected.out
|
|
|
|
structSorryBug.lean
|
chore: simplify option names
|
2022-02-08 12:23:24 -08:00 |
|
structSorryBug.lean.expected.out
|
feat: improve error when an identifier is unbound because autoImplicit is off (#11119)
|
2025-11-19 03:11:34 +00:00 |
|
StxQuot.lean
|
|
|
|
StxQuot.lean.expected.out
|
chore: minor module system fixes from batteries port (#10496)
|
2025-09-24 08:59:23 +00:00 |
|
substFails.lean
|
|
|
|
substFails.lean.expected.out
|
|
|
|
syntaxErrors.lean
|
|
|
|
syntaxErrors.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
syntaxInNamespacesAndPP.lean
|
|
|
|
syntaxInNamespacesAndPP.lean.expected.out
|
feat: overhaul meta system (#10362)
|
2025-09-17 21:04:29 +00:00 |
|
syntaxPrec.lean
|
|
|
|
syntaxPrec.lean.expected.out
|
fix: local syntax should create private definitions
|
2025-08-19 14:49:12 -07:00 |
|
syntheticHolesAsPatterns.lean
|
|
|
|
syntheticHolesAsPatterns.lean.expected.out
|
|
|
|
syntheticOpaqueReadOnly.lean
|
|
|
|
syntheticOpaqueReadOnly.lean.expected.out
|
|
|
|
synthorder.lean
|
|
|
|
synthorder.lean.expected.out
|
|
|
|
tabulate.lean
|
|
|
|
tabulate.lean.expected.out
|
|
|
|
tacUnsolvedGoalsErrors.lean
|
|
|
|
tacUnsolvedGoalsErrors.lean.expected.out
|
|
|
|
tcloop.lean
|
|
|
|
tcloop.lean.expected.out
|
|
|
|
termination_by.lean
|
|
|
|
termination_by.lean.expected.out
|
feat: "try this" messages with support for interactivity (#10524)
|
2025-10-13 13:39:03 +00:00 |
|
termination_by_vars.lean
|
|
|
|
termination_by_vars.lean.expected.out
|
|
|
|
termination_by_where.lean
|
|
|
|
termination_by_where.lean.expected.out
|
|
|
|
terminationFailure.lean
|
|
|
|
terminationFailure.lean.expected.out
|
|
|
|
test_extern.lean
|
|
|
|
test_extern.lean.expected.out
|
|
|
|
test_single.sh
|
fix: detect private references in inferred type of public def (#10762)
|
2025-10-15 12:51:54 +00:00 |
|
theoremType.lean
|
|
|
|
theoremType.lean.expected.out
|
|
|
|
thunk.lean
|
|
|
|
thunk.lean.expected.out
|
|
|
|
toExpr.lean
|
|
|
|
toExpr.lean.expected.out
|
|
|
|
toFieldNameIssue.lean
|
|
|
|
toFieldNameIssue.lean.expected.out
|
|
|
|
tokenErrors.lean
|
chore: simplify tests
|
2021-04-05 22:01:56 +02:00 |
|
tokenErrors.lean.expected.out
|
|
|
|
tooManyVarsAtInduction.lean
|
|
|
|
tooManyVarsAtInduction.lean.expected.out
|
chore: error messages consistency (#10143)
|
2025-08-26 17:55:43 +00:00 |
|
traceClassScopes.lean
|
|
|
|
traceClassScopes.lean.expected.out
|
|
|
|
traceStateBacktracking.lean
|
chore: fix spelling errors (#10042)
|
2025-08-22 07:23:12 +00:00 |
|
traceStateBacktracking.lean.expected.out
|
chore: fix spelling errors (#10042)
|
2025-08-22 07:23:12 +00:00 |
|
traceTacticSteps.lean
|
chore: add test
|
2021-11-30 15:34:54 +01:00 |
|
traceTacticSteps.lean.expected.out
|
feat: use with_trace for important trace classes
|
2023-04-10 16:57:54 +02:00 |
|
trailingComma.lean
|
feat: linter.unusedSimpArgs (#8901)
|
2025-06-22 09:10:21 +00:00 |
|
trailingComma.lean.expected.out
|
feat: linter.unusedSimpArgs (#8901)
|
2025-06-22 09:10:21 +00:00 |
|
treeMap.lean
|
|
|
|
treeMap.lean.expected.out
|
feat: nested well-founded recursion via automatic preprocessing (#6744)
|
2025-02-10 16:43:41 +00:00 |
|
typeIncorrectPat.lean
|
|
|
|
typeIncorrectPat.lean.expected.out
|
fix: preserve error locations when expanding match arms (#10783)
|
2025-10-15 13:31:42 +00:00 |
|
typeMismatch.lean
|
|
|
|
typeMismatch.lean.expected.out
|
|
|
|
typeOf.lean
|
|
|
|
typeOf.lean.expected.out
|
feat: improve error message in the case of type class synthesis failure (#11245)
|
2025-11-21 21:24:27 +00:00 |
|
uintCtors.lean
|
chore: remove >6 month old deprecations (#10446)
|
2025-09-22 12:47:11 +00:00 |
|
uintCtors.lean.expected.out
|
|
|
|
uintMatch.lean
|
fix: pattern matching on UInt
|
2021-09-05 19:15:59 -07:00 |
|
uintMatch.lean.expected.out
|
|
|
|
unboxStruct.lean
|
|
|
|
unboxStruct.lean.expected.out
|
feat: zero cost BaseIO (#10625)
|
2025-10-22 10:55:12 +02:00 |
|
unexpander.lean
|
|
|
|
unexpander.lean.expected.out
|
|
|
|
unexpandersNamespaces.lean
|
|
|
|
unexpandersNamespaces.lean.expected.out
|
|
|
|
UnexpandSubtype.lean
|
|
|
|
UnexpandSubtype.lean.expected.out
|
|
|
|
unfold1.lean
|
|
|
|
unfold1.lean.expected.out
|
|
|
|
unfoldDefEq.lean
|
|
|
|
unfoldDefEq.lean.expected.out
|
|
|
|
unfoldFailure.lean
|
|
|
|
unfoldFailure.lean.expected.out
|
|
|
|
unfoldReduceMatch.lean
|
|
|
|
unfoldReduceMatch.lean.expected.out
|
|
|
|
unhygienic.lean
|
|
|
|
unhygienic.lean.expected.out
|
|
|
|
unhygienicCode.lean
|
|
|
|
unhygienicCode.lean.expected.out
|
chore: rename Substring to Substring.Raw (#11154)
|
2025-11-16 09:30:04 +00:00 |
|
unifHintAndTC.lean
|
|
|
|
unifHintAndTC.lean.expected.out
|
feat: add option pp.piBinderNames (#10374)
|
2025-09-14 05:15:04 +00:00 |
|
univInference.lean
|
|
|
|
univInference.lean.expected.out
|
|
|
|
unknownId.lean
|
|
|
|
unknownId.lean.expected.out
|
|
|
|
unknownTactic.lean
|
chore: adapt stdlib & tests
|
2021-05-20 15:17:36 -07:00 |
|
unknownTactic.lean.expected.out
|
|
|
|
unnecessaryUnfolding.lean
|
|
|
|
unnecessaryUnfolding.lean.expected.out
|
|
|
|
unsolvedIndCases.lean
|
|
|
|
unsolvedIndCases.lean.expected.out
|
|
|
|
unused_univ.lean
|
|
|
|
unused_univ.lean.expected.out
|
|
|
|
unusedLet.lean
|
|
|
|
unusedLet.lean.expected.out
|
|
|
|
unusedWarningAtStructUpdate.lean
|
feat: add missingDocs linter
|
2022-07-31 18:18:21 -07:00 |
|
unusedWarningAtStructUpdate.lean.expected.out
|
|
|
|
updateExprIssue.lean
|
refactor: use computed fields for Expr
|
2022-07-11 14:19:41 -07:00 |
|
updateExprIssue.lean.expected.out
|
|
|
|
updateLevelIssues.lean
|
fix: Level.update* functions
|
2022-07-10 09:16:02 -07:00 |
|
updateLevelIssues.lean.expected.out
|
fix: Level.update* functions
|
2022-07-10 09:16:02 -07:00 |
|
Uri.lean
|
refactor: use String.Slice in String.take and variants (#11180)
|
2025-11-18 16:13:48 +00:00 |
|
Uri.lean.expected.out
|
|
|
|
versoDocMissing.lean
|
fix: better error message on missing declaration name for docstring (#10608)
|
2025-09-29 06:26:08 +00:00 |
|
versoDocMissing.lean.expected.out
|
feat: user extensibility in try? (#11149)
|
2025-11-12 23:49:54 +00:00 |
|
warningAsError.lean
|
|
|
|
warningAsError.lean.expected.out
|
|
|
|
wf1.lean
|
|
|
|
wf1.lean.expected.out
|
|
|
|
wf2.lean
|
|
|
|
wf2.lean.expected.out
|
|
|
|
wfrecUnusedLet.lean
|
|
|
|
wfrecUnusedLet.lean.expected.out
|
|
|
|
whnfProj.lean
|
|
|
|
whnfProj.lean.expected.out
|
|
|
|
wildcardAlt.lean
|
|
|
|
wildcardAlt.lean.expected.out
|
|
|
|
withAssignableSyntheticOpaqueBug.lean
|
|
|
|
withAssignableSyntheticOpaqueBug.lean.expected.out
|
|
|
|
withLocation.lean
|
|
|
|
withLocation.lean.expected.out
|
|
|
|
withLocationImplementationDetails.lean
|
|
|
|
withLocationImplementationDetails.lean.expected.out
|
|
|
|
withSetOptionIn.lean
|
feat: guard_msgs to treat trace messages separate (#8267)
|
2025-05-09 05:44:34 +00:00 |
|
withSetOptionIn.lean.expected.out
|
|
|
|
workspaceSymbols.lean
|
|
|
|
workspaceSymbols.lean.expected.out
|
|
|
|
xmlParsing.lean
|
|
|
|
xmlParsing.lean.expected.out
|
|
|
|
zipper.lean
|
|
|
|
zipper.lean.expected.out
|
|
|
