Joachim Breitner 10d6232594 chore: remove test for #10766 (#10804) ... the tested situation (kernel runs into deep recursion but elaborator is happy) is not very stable and depends on, for example, stack size. This test is not worth that hassle.		2025-10-16 11:11:29 +00:00
..
docparse	fix: trailing whitespace setting for string literals was ignored (#10389)	2025-09-15 09:51:56 +00:00
grind	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
interactive	fix: unknown identifier minimization (#10797)	2025-10-15 19:25:27 +00:00
Reformat
run	chore: remove test for #10766 (#10804)	2025-10-16 11:11:29 +00:00
server	test: improve language server test coverage (#10574)	2025-09-30 11:15:03 +00:00
trust0
.gitignore	chore: ignore test output files	2020-08-31 11:09:27 +02:00
217.lean	fix: fixes #217	2020-11-12 14:36:47 -08:00
217.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
220.lean	fix: fixes #220 and #223	2020-11-24 10:18:02 -08:00
220.lean.expected.out
223.lean	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
223.lean.expected.out	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
236.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
236.lean.expected.out
241.lean	fix: fixes #241	2021-05-22 19:10:07 -07:00
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	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
247.lean	fix: fixes #247	2021-04-15 12:33:45 -07:00
247.lean.expected.out
248.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
248.lean.expected.out	refactor: update and consolidate attribute-related error messages (#9495)	2025-07-26 02:03:18 +00:00
255.lean	feat: allow hygienic capture of section variables in quotations	2021-01-24 11:46:04 -08:00
255.lean.expected.out	feat: note inaccessible private declarations in unknown constant error (#9516)	2025-07-25 09:23:52 +00:00
276.lean	fix: make elabAsElim aware of explicit motive arguments (#4817)	2024-07-29 19:18:47 +00:00
276.lean.expected.out	feat: add option pp.piBinderNames (#10374)	2025-09-14 05:15:04 +00:00
277a.lean	chore: fix spelling mistakes in tests (#5439)	2024-09-24 03:22:53 +00:00
277a.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
277b.lean	fix: do not evaluate code containing sorry	2021-01-26 15:01:53 -08:00
277b.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
283.lean	fix: solve method at isLevelDefEq	2021-01-20 08:36:26 -08:00
283.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
297.lean	fix: missing checkAssignment at assignToConstFun	2021-01-26 17:33:33 -08:00
297.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
301.lean	fix: missing occursCheck at SyntheticMVars	2021-01-29 17:13:04 -08:00
301.lean.expected.out
302.lean	fix: fixes #302	2021-02-03 15:04:18 -08:00
302.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
307.lean	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
307.lean.expected.out
309.lean	fix: make sure kernel checks examples	2021-02-25 13:34:27 -08:00
309.lean.expected.out
331.lean	feat: allow optional type in example	2022-09-13 03:11:04 -07:00
331.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
345.lean.expected.out
346.lean	chore: improve error message	2021-03-16 20:42:38 -07:00
346.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
348.lean	fix: fixes #348	2021-03-16 17:50:40 -07:00
348.lean.expected.out
353.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
353.lean.expected.out
361.lean	chore: fix test	2022-01-31 16:45:57 -08:00
361.lean.expected.out
366.lean	fix: fixes #366	2021-03-23 16:02:45 -07:00
366.lean.expected.out
386.lean	fix: fixes #386	2021-04-11 20:57:39 -07:00
386.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
389.lean	test: expand test for 389	2021-04-11 20:55:33 -07:00
389.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
414.lean	chore: fix tests	2022-04-01 11:34:50 -07:00
414.lean.expected.out
415.lean	chore: fix tests	2022-06-27 22:37:02 +02:00
415.lean.expected.out
421.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
421.lean.expected.out
423.lean	test: add second example for issue #423	2021-04-25 10:35:23 -07:00
423.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
435.lean	fix: fixes #435	2021-05-02 18:16:57 -07:00
435.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
435b.lean	fix: add basic support for accessing the field of a section variable in the notation prechecker	2021-05-04 22:41:25 -07:00
435b.lean.expected.out
439.lean.expected.out
440.lean	feat: closes #440	2021-05-15 20:54:54 -07:00
440.lean.expected.out
445.lean	refactor: simplify runTermElabM and liftTermElabM	2022-08-07 07:35:02 -07:00
445.lean.expected.out	feat: transform nondependent lets into haves in declarations and equation lemmas (#8373)	2025-06-29 19:45:45 +00:00
448.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
448.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
449.lean	fix: fixes #449	2021-05-10 13:10:59 -07:00
449.lean.expected.out
450.lean	fix: fixes #450	2021-05-10 13:55:06 -07:00
450.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
469.lean	feat: apply app unexpanders for all prefixes of an application (#3375)	2024-02-27 07:04:17 +00:00
469.lean.expected.out
474.lean	feat: better #eval command (#5627)	2024-10-08 20:51:46 +00:00
474.lean.expected.out
490.lean	fix: _root_ prefix in declarations	2022-06-13 14:03:18 -07:00
490.lean.expected.out
496.lean	chore: improve error message when compiling code containing axioms or noncomputable definitions	2021-05-31 20:27:15 -07:00
496.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
529.lean	feat: add withOpenDecl and withOpen parsers	2021-08-22 20:50:35 -07:00
529.lean.expected.out
550.lean	fix: offset support at isDefEq should not use HAdd.hAdd	2021-07-27 16:16:03 -07:00
550.lean.expected.out
586.lean	fix: ensure hygiene of double-quoted names	2021-07-30 07:17:50 -07:00
586.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
593.lean	fix: fixes #593	2021-08-02 10:46:12 -07:00
593.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
603.lean.expected.out
604.lean	fix: fixes #604	2021-08-04 17:19:17 -07:00
604.lean.expected.out
620.lean
620.lean.expected.out
621.lean	feat: shorten auto-generated instance names (#3089)	2024-04-13 18:08:50 +00:00
621.lean.expected.out	refactor: update and consolidate attribute-related error messages (#9495)	2025-07-26 02:03:18 +00:00
625.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
625.lean.expected.out
641.lean	feat: improved name-unresolving in delab	2021-09-07 16:26:00 +02:00
641.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
653.lean	fix: fixes #653	2021-09-04 18:42:33 -07:00
653.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
655.lean	fix: fixes #655	2021-09-07 12:17:28 -07:00
655.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
679.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
679.lean.expected.out
689.lean	fix: panic messages on invalid input	2021-09-25 09:01:01 -07:00
689.lean.expected.out
690.lean	fix: check number of explicit variables at induction/cases alternatives when @ is not used	2021-09-29 07:39:38 -07:00
690.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
697.lean	feat: reject partial when if constant is not a function	2021-09-28 21:07:14 -07:00
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	fix: make sure monad lift coercion elaborator has no side effects (#6024)	2024-11-13 16:22:31 +00:00
755.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
770.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
770.lean.expected.out
799.lean	fix: generate an error if declaration name clashes with variable name	2022-01-10 12:08:11 -08:00
799.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
801.lean	test: wrong test	2022-02-02 13:17:30 +01:00
801.lean.expected.out
813.lean	fix: remove @[reducible] annotation from Function.comp and Function.const	2021-11-23 07:29:25 -08:00
813.lean.expected.out	fix: discrepancy theorem vs example (#4493)	2024-06-24 01:18:41 +00:00
815b.lean	chore: fix tests	2022-08-15 08:55:25 -07:00
815b.lean.expected.out	feat: suppress safe shadowing within fun binders (#10376)	2025-09-14 15:54:59 +00:00
906.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
906.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
916.lean	test: for #916	2022-01-03 07:57:16 -08:00
916.lean.expected.out
948.lean	feat: grind internal CommRing class (#7797)	2025-04-03 08:30:19 +00:00
948.lean.expected.out
951.lean	feat: shorten auto-generated instance names (#3089)	2024-04-13 18:08:50 +00:00
951.lean.expected.out
973.lean	feat: generate error message for simp theorems that are equivalent to x = x	2022-01-26 11:16:31 -08:00
973.lean.expected.out
973b.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
973b.lean.expected.out
995.lean	fix: match tactic should not trigger implicit lambdas	2022-02-04 07:55:56 -08:00
995.lean.expected.out
1007.lean	chore: fix spelling mistakes in tests (#5439)	2024-09-24 03:22:53 +00:00
1007.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
1011.lean	feat: allow upper case single character identifiers when relaxedAutoImplicit false (#2277)	2023-06-19 20:04:09 -07:00
1011.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
1021.lean	fix: nasty bug at findDeclarationRangesCore?	2022-03-19 16:53:22 -07:00
1021.lean.expected.out	fix: let anonymous constructor notation elaborate with insufficient arguments (#10391)	2025-09-15 16:44:34 +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	fix: toName function at elabAppFnId	2022-03-04 16:56:02 -08:00
1038.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +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	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1050.lean.expected.out
1057.lean	fix: check type mismatch at dependent pattern matching compiler	2022-03-21 09:28:02 -07:00
1057.lean.expected.out	fix: preserve error locations when expanding match arms (#10783)	2025-10-15 13:31:42 +00:00
1062.lean	test: for issue #1062	2022-03-22 14:14:28 -07:00
1062.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
1074b.lean	feat: infer Prop for inductive/structure when defining syntactic subsingletons (#5517)	2024-10-08 22:39:38 +00:00
1074b.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
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	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
1081.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
1098.lean	feat: make #check <ident> always show the signature without elaboration	2022-12-21 21:59:05 +01:00
1098.lean.expected.out
1102.lean	feat: reorder tc subgoals according to out-params	2023-04-10 13:00:04 -07:00
1102.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
1112.lean	fix: index out of bounds at computeFixedIndexBitMask	2022-04-19 05:21:43 -07:00
1112.lean.expected.out
1113.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
1113.lean.expected.out
1163.lean.expected.out
1206.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
1206.lean.expected.out
1235.lean	fix: remove kabstractWithPred	2022-06-20 16:35:18 -07:00
1235.lean.expected.out
1240.lean	feat: module header keyword for enabling module system	2025-04-21 18:40:11 +02:00
1240.lean.expected.out
1275.lean	fix: wrap &"..." <|> ... as well	2022-10-28 21:25:47 +02:00
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	fix: dependent pattern matching bug	2022-07-03 13:25:12 -07:00
1279.lean.expected.out
1279_simplified.lean
1279_simplified.lean.expected.out
1292.lean	fix: bug at the code specialization cache	2022-07-07 22:59:18 -07:00
1292.lean.expected.out
1298.lean	chore: upstream NatCast and IntCast (#3347)	2024-02-16 00:54:22 +00:00
1298.lean.expected.out
1301.lean	test: for issue #1301	2022-07-13 06:05:12 -07:00
1301.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
1321.lean	test: for issue #1321	2022-07-18 23:50:41 -04:00
1321.lean.expected.out	feat: overhaul meta system (#10362)	2025-09-17 21:04:29 +00:00
1358.lean	fix: ensure messages associated with last exception are not lost at evalTactic	2022-07-22 12:05:29 -04:00
1358.lean.expected.out
1363.lean	chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115)	2024-08-21 15:26:17 +00:00
1363.lean.expected.out	refactor: update and consolidate attribute-related error messages (#9495)	2025-07-26 02:03:18 +00:00
1367.lean	fix: notation delaborator on over-application	2022-07-25 13:42:37 -07:00
1367.lean.expected.out
1371.lean	fix: unused match-syntax alternatives are silently ignored	2022-07-31 06:00:08 -07:00
1371.lean.expected.out	fix: unused match-syntax alternatives are silently ignored	2022-07-31 06:00:08 -07:00
1377.lean	fix: preserve user-facing names and BinderInfo when lifting let-rec declarations	2022-07-28 06:36:45 -07:00
1377.lean.expected.out
1433.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
1433.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
1569.lean	fix: disable auto implicit feature when running tactics	2022-09-09 15:17:50 -07:00
1569.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
1571.lean	fix: fixes #1571	2022-09-15 11:16:16 -07:00
1571.lean.expected.out
1576.lean	fix: fixes #1576	2022-09-09 14:29:48 -07:00
1576.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
1606.lean	feat: use colEq in sepByIndent	2022-09-19 12:44:43 -07:00
1606.lean.expected.out
1616.lean	fix: stop iterating over visited mvars in collectUnassignedMVars	2023-05-15 09:37:19 -07:00
1616.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
1657.lean	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
1657.lean.expected.out	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
1668.lean	fix: derive Repr missing a comma	2022-10-01 07:17:57 -07:00
1668.lean.expected.out
1673.lean	fix: fixes #1673	2022-10-02 08:23:14 -07:00
1673.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
1681.lean	fix: fixes #1681	2022-10-07 18:36:25 -07:00
1681.lean.expected.out
1682.lean	feat: sort refine new goals using the order they were created	2022-10-04 06:54:14 -07:00
1682.lean.expected.out
1690.lean	fix: avoid nontermination on non-utf8 input	2022-10-06 17:45:21 -07:00
1690.lean.expected.out
1705.lean	fix: fixes #1705	2022-10-07 13:11:26 -07:00
1705.lean.expected.out	feat: allow structures to have non-bracketed binders (#8671)	2025-06-17 17:40:18 +00:00
1707.lean	fix: fixes #1707	2022-10-08 07:58:56 -07:00
1707.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
1719.lean	feat: improve apply error message when root term elaboration is postponed	2022-10-26 17:15:24 -07:00
1719.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
1760.lean	fix: do not create choice nodes for failed parses	2022-11-11 09:13:02 +01:00
1760.lean.expected.out
1763.lean	feat: congr theorems using Iff	2022-10-26 18:00:24 -07:00
1763.lean.expected.out
1779.lean	feat: use unop% to implement unary minus notation	2022-10-26 06:55:24 -07:00
1779.lean.expected.out
1781.lean	fix: bug in level normalization (soundness bug)	2022-10-26 05:22:26 -07:00
1781.lean.expected.out
1804.lean	feat: allow doSeq in let x <- e | seq	2022-11-08 08:29:21 -08:00
1804.lean.expected.out
1825.lean	fix: integer overflows	2022-11-15 07:37:54 -08:00
1825.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
1845.lean	fix: do method lifting across choice nodes	2022-11-21 17:52:14 +01:00
1845.lean.expected.out
1856.lean	fix: fixes #1856	2022-11-18 19:34:32 -08:00
1856.lean.expected.out
1878.lean	test: for #1878	2022-11-24 13:03:45 -08:00
1878.lean.expected.out
1891.lean	fix: fixes #1891	2022-11-29 08:59:46 -08:00
1891.lean.expected.out
1918.lean	fix: remove repeat calls to inferType in ignoreField	2023-05-15 09:35:44 -07:00
1918.lean.expected.out
1971.lean	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
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	fix: fixes #2006	2023-01-04 08:19:22 -08:00
2006.lean.expected.out
2045.lean	feat: apply app unexpanders for all prefixes of an application (#3375)	2024-02-27 07:04:17 +00:00
2045.lean.expected.out
2077.lean	fix: fixes #2077	2023-06-30 19:26:00 -07:00
2077.lean.expected.out
2115.lean	chore: fix test file names	2023-07-01 06:20:36 -07:00
2115.lean.expected.out
2125.lean	fix: reject occurrences of inductive type in index	2023-02-28 12:22:54 -08:00
2125.lean.expected.out
2178.lean	chore: upstream Zero and NeZero	2024-09-10 19:30:09 +10:00
2178.lean.expected.out	fix: fixes #2178 (#2784)	2023-10-30 15:06:56 +11:00
2273.lean	feat: add flag for apply to defer failed typeclass syntheses as goals	2023-06-19 20:07:07 -07:00
2273.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
2361.lean	feat: withAssignableSyntheticOpaque in assumption (#2596)	2023-10-30 04:00:52 +00:00
2361.lean.expected.out
2505.lean	chore: fix MVarId.getType' (#2595)	2023-10-09 11:04:33 +00:00
2505.lean.expected.out
2514.lean	fix: dsimp missing consumeMData when closing goals by rfl (#2776)	2023-10-30 09:32:32 +11:00
2514.lean.expected.out
2634.lean	fix: simp fails when custom discharger makes no progress (#3317)	2024-02-17 13:42:04 +00:00
2634.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
3057.lean	feat: .ctorIdx for all inductives (#9951)	2025-08-25 10:47:06 +00:00
3057.lean.expected.out
3140.lean	fix: derive BEq on structure with Prop-fields (#3191)	2024-01-18 02:32:51 +00:00
3140.lean.expected.out
3989_1.lean
3989_1.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
3989_2.lean
3989_2.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
4089.lean	feat: relaxed reset/reuse in the code generator (#4100)	2024-05-07 22:08:32 +00:00
4089.lean.expected.out	chore: add a new tagged IRType for inline tagged scalars (#9394)	2025-07-16 00:42:56 +00:00
4117.lean	fix: add checkSystem and withIncRecDepth to withAutoBoundImplicit (#4128)	2024-05-10 21:55:26 +00:00
4117.lean.expected.out
4240.lean	fix: accidental ownership with specialization	2024-06-07 13:59:22 +02:00
4240.lean.expected.out	chore: add a new tagged IRType for inline tagged scalars (#9394)	2025-07-16 00:42:56 +00:00
4309.lean	fix: panic when applying @[simp] to malformed theorem syntax (#4341)	2024-06-04 16:52:26 +00:00
4309.lean.expected.out
4375.lean	fix: kernel exception from fvars left from ?m a b instantiation (#4410)	2024-06-10 19:02:27 +00:00
4375.lean.expected.out
4452.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
4452.lean.expected.out	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
4591.lean	fix: unresolve name avoiding locals (#4593)	2024-07-02 01:15:39 +00:00
4591.lean.expected.out	feat: "try this" messages with support for interactivity (#10524)	2025-10-13 13:39:03 +00:00
4845.lean	fix: wildcard generalize only generalizes visible theorems (#4846)	2024-10-25 05:09:28 +00:00
4845.lean.expected.out
6601.lean	fix: allow dot idents to resolve to local names (#6602)	2025-01-12 17:18:22 +00:00
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	chore: fix tests	2021-09-07 19:14:30 -07:00
abst.lean.expected.out
allFieldForConstants.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
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
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	chore: avoid Has prefix in type classes	2020-10-27 18:29:19 -07:00
attrCmd.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
autobound_and_macroscopes.lean
autobound_and_macroscopes.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
autoBoundErrorMsg.lean
autoBoundErrorMsg.lean.expected.out
autoBoundImplicits1.lean
autoBoundImplicits1.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
autoBoundImplicits2.lean
autoBoundImplicits2.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
autoBoundPostponeLoop.lean
autoBoundPostponeLoop.lean.expected.out
autoImplicitChain.lean
autoImplicitChain.lean.expected.out
autoImplicitChainNameIssue.lean
autoImplicitChainNameIssue.lean.expected.out
autoImplicitCtorParamIssue.lean
autoImplicitCtorParamIssue.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
autoImplicitForbidden.lean
autoImplicitForbidden.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
autoIssue.lean
autoIssue.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
autoPPExplicit.lean
autoPPExplicit.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
auxDeclIssue.lean
auxDeclIssue.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
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	fix: make IO.RealWorld opaque (#9631)	2025-09-08 18:12:19 +00:00
beginEndAsMacro.lean
beginEndAsMacro.lean.expected.out
bigUnivOffsets.lean
bigUnivOffsets.lean.expected.out	chore: break up universe level error message (#9637)	2025-07-30 23:52:53 +00:00
binder_predicates.lean
binder_predicates.lean.expected.out
binderCacheIssue.lean
binderCacheIssue.lean.expected.out
binderCacheIssue2.lean
binderCacheIssue2.lean.expected.out
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	fix: binop% info tree	2023-01-16 08:33:58 -08:00
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	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
binrel_binop.lean
binrel_binop.lean.expected.out
binrelTypeMismatch.lean
binrelTypeMismatch.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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	feat: Bool.to(U)IntX (#6060)	2024-11-13 15:49:16 +00:00
bool2int.lean.expected.out
bool_simp.lean
bool_simp.lean.expected.out
bootstrapSorry.lean	chore: fix failing mk*Sorry in bootstrapping contexts (#9950)	2025-08-17 16:14:53 +00:00
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	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
calcErrors.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
casesOnCases.lean
casesOnCases.lean.expected.out
caseSuggestions.lean	feat: add case name hints (#9316)	2025-07-17 03:22:30 +00:00
caseSuggestions.lean.expected.out	feat: add case name hints (#9316)	2025-07-17 03:22:30 +00:00
cdotTuple.lean
cdotTuple.lean.expected.out
class_def_must_fail.lean
class_def_must_fail.lean.expected.out
classBadOutParam.lean
classBadOutParam.lean.expected.out
coe.lean	fix: extended coe notation and delaborator (#3295)	2024-02-10 04:58:28 +00:00
coe.lean.expected.out
coeAttr1.lean	chore: upstream Std.Tactic.CoeExt to Lean.Elab.CoeExt (#3280)	2024-02-09 04:55:49 +00:00
coeAttr1.lean.expected.out
coeM.lean	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
coeM.lean.expected.out
collectDepsIssue.lean
collectDepsIssue.lean.expected.out
commandPrefix.lean
commandPrefix.lean.expected.out
computedFieldsCode.lean
computedFieldsCode.lean.expected.out	feat: T.ctor.elim single-constructor cases function (#9952)	2025-08-27 09:40:31 +00:00
congrThm.lean
congrThm.lean.expected.out
congrThmIssue.lean
congrThmIssue.lean.expected.out
constDelab.lean
constDelab.lean.expected.out
constructorTac.lean
constructorTac.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
consumePPHint.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
consumePPHint.lean.expected.out	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
conv1.lean	feat: in conv tactic, use try with_reducibe rfl (#3763)	2024-03-29 11:59:45 +00:00
conv1.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
convInConv.lean
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
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	chore: adopt tobject IRType (#9392)	2025-07-15 23:56:49 +00:00
csimpAttrAppend.lean
csimpAttrAppend.lean.expected.out	chore: adopt tobject IRType (#9392)	2025-07-15 23:56:49 +00:00
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	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
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: use match decEq, not if h : in deriving DecidableEq (#10274)	2025-09-06 21:00:34 +00:00
decimals.lean
decimals.lean.expected.out
decreasing_by.lean
decreasing_by.lean.expected.out	perf: check simp cache in simpLoop (#8880)	2025-06-21 17:58:05 +00:00
defaultInstance.lean
defaultInstance.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
defaultInstanceWithPrio.lean
defaultInstanceWithPrio.lean.expected.out
defInst.lean	feat: make delta deriving more robust and handle binders (#9800)	2025-08-10 21:21:54 +00:00
defInst.lean.expected.out	feat: make delta deriving more robust and handle binders (#9800)	2025-08-10 21:21:54 +00:00
delabDoLetFun.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
delabDoLetFun.lean.expected.out
delabOverApp.lean
delabOverApp.lean.expected.out
delabUnexpand.lean
delabUnexpand.lean.expected.out
delta.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
delta.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
deltaRedIndPredBelow.lean
deltaRedIndPredBelow.lean.expected.out
deprecated.lean
deprecated.lean.expected.out	feat: note potential discrepancies in deprecation warning (#9606)	2025-07-31 16:41:14 +00:00
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
derivingRpcEncoding.lean.expected.out
diamond1.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
diamond1.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
diamond2.lean	feat: structure instance notation elaboration improvements (#7717)	2025-03-30 17:40:36 +00:00
diamond2.lean.expected.out
diamond3.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
diamond3.lean.expected.out
diamond4.lean	fix: binder annotation for class diamond coercions	2021-08-10 06:59:28 -07:00
diamond4.lean.expected.out
diamond5.lean	feat: make structure parent projections nameable (#7100)	2025-02-18 07:38:13 +00:00
diamond5.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
diamond6.lean	feat: make #check <ident> always show the signature without elaboration	2022-12-21 21:59:05 +01:00
diamond6.lean.expected.out
diamond7.lean	chore: upstream Inv notation typeclass (#8345)	2025-05-15 03:56:23 +00:00
diamond7.lean.expected.out
diamond8.lean	feat: grind internal CommRing class (#7797)	2025-04-03 08:30:19 +00:00
diamond8.lean.expected.out
diamond9.lean	chore: upstream Zero and NeZero	2024-09-10 19:30:09 +10:00
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
doErrorMsg.lean
doErrorMsg.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
doIfLet.lean	feat: support let mut x := e | alt	2022-08-10 06:29:49 -07:00
doIfLet.lean.expected.out
doIssue.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
doIssue.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
doLetLoop.lean
doLetLoop.lean.expected.out
doNotation1.lean
doNotation1.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
doSeqRightIssue.lean	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
doSeqRightIssue.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
doubleReset.lean
doubleReset.lean.expected.out	feat: default let rec and where decls to private under the module system (#9759)	2025-08-06 15:53:51 +00:00
dsimpViaConst.lean
dsimpViaConst.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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
eagerUnfoldingIssue.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
ellipsisProjIssue.lean
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
elseifDoErrorPos.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
emptyc.lean	chore: avoid Has prefix in type classes	2020-10-27 18:29:19 -07:00
emptyc.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
emptyTypeAscription.lean
emptyTypeAscription.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
eoi.lean	chore: improve EOI error message	2021-04-03 11:56:26 +02:00
eoi.lean.expected.out
eraseInsts.lean
eraseInsts.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
eraseSimp.lean
eraseSimp.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
errorOnInductionForNested.lean
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
eta.lean	feat: add Expr.eta	2021-04-09 14:21:21 -07:00
eta.lean.expected.out
etaReducedMvarAssignments.lean
etaReducedMvarAssignments.lean.expected.out
etaStructIssue.lean
etaStructIssue.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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
evalInstMessage.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
evalLeak.lean
evalLeak.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
evalNone.lean
evalNone.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
evalSorry.lean
evalSorry.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
evalWithMVar.lean
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
extract.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
extract.lean.expected.out
failTac.lean	fix: display all remaining goals at fail tactic error message	2022-02-26 09:49:06 -08:00
failTac.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
file_not_found.lean
file_not_found.lean.expected.out
filePath.lean
filePath.lean.expected.out
fixedIndexToParamIssue.lean
fixedIndexToParamIssue.lean.expected.out
fixedIndicesToParams.lean
fixedIndicesToParams.lean.expected.out
forallMetaBounded.lean
forallMetaBounded.lean.expected.out
forErrors.lean
forErrors.lean.expected.out	chore: rename Stream to Std.Stream (#10645)	2025-10-02 15:25:56 +00:00
Format.lean	chore: remove remaining #lang lean4 in tests	2021-01-27 14:45:31 +01:00
Format.lean.expected.out
formatTerm.lean
formatTerm.lean.expected.out
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	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
funind_errors.lean	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
funind_errors.lean.expected.out	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
funind_reserved.lean
funind_reserved.lean.expected.out
funInfoBug.lean
funInfoBug.lean.expected.out
funParen.lean	fix: fun (x ...) ... should not be treated as a pattern	2022-04-15 10:00:26 -07:00
funParen.lean.expected.out
gcd.lean	feat: add Nat.gcd	2021-03-07 18:47:02 -08:00
gcd.lean.expected.out
getElem.lean	feat: redefine Range.forIn' (#6390)	2024-12-15 09:47:50 +00:00
getElem.lean.expected.out
guessLex.lean
guessLex.lean.expected.out
guessLexDiff.lean
guessLexDiff.lean.expected.out
guessLexFailures.lean
guessLexFailures.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
guessLexTricky.lean
guessLexTricky.lean.expected.out
guessLexTricky2.lean
guessLexTricky2.lean.expected.out
have.lean	feat: have: remove unnecessary whitespace check and allow name- and type-less have	2021-05-25 14:25:14 +02:00
have.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
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	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
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
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
inductionGen.lean.expected.out
inductionMutual.lean
inductionMutual.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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
inductiveUnivErrorMsg.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
indUsingTerm.lean
indUsingTerm.lean.expected.out
inlineIssue.lean
inlineIssue.lean.expected.out
inst.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
inst.lean.expected.out
instance1.lean
instance1.lean.expected.out	feat: add hints for missing structure instance fields (#9317)	2025-07-17 03:22:34 +00:00
int_div_mod.lean
int_div_mod.lean.expected.out
intModBug.lean
intModBug.lean.expected.out
intNegSucc.lean
intNegSucc.lean.expected.out
introLetBug.lean
introLetBug.lean.expected.out
invalidFieldName.lean
invalidFieldName.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
invalidInstImplicit.lean
invalidInstImplicit.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
invalidMutualError.lean
invalidMutualError.lean.expected.out
invalidNamedArgs.lean	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
invalidNamedArgs.lean.expected.out	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
invalidPatternIssue.lean
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	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
isNoncomputable.lean
isNoncomputable.lean.expected.out
issue2260.lean
issue2260.lean.expected.out
issue2981.lean
issue2981.lean.expected.out
issue3232.lean
issue3232.lean.expected.out	feat: improve split error messages (#9424)	2025-07-18 22:36:10 +00:00
jason2.lean	fix: missing error messages	2021-03-05 17:20:04 -08:00
jason2.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
jpCasesDiscrM.lean	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
jpCasesDiscrM.lean.expected.out	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
jpCasesNary.lean	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
jpCasesNary.lean.expected.out	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
jpClosureIssue.lean	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
jpClosureIssue.lean.expected.out	fix: make IO.RealWorld opaque (#9631)	2025-09-08 18:12:19 +00:00
json.lean
json.lean.expected.out
kernelMVarBug.lean
kernelMVarBug.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +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	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
lazySeq.lean	test: add *> laziness test	2021-09-07 18:03:15 -07:00
lazySeq.lean.expected.out
lcnfTypes.lean
lcnfTypes.lean.expected.out	fix: make IO.RealWorld opaque (#9631)	2025-09-08 18:12:19 +00: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	feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)	2025-06-22 21:54:57 +00:00
letPatIssue.lean
letPatIssue.lean.expected.out
letrec1.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
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
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	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
linterSuspiciousUnexpanderPatterns.lean
linterSuspiciousUnexpanderPatterns.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
linterUnusedVariables.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
linterUnusedVariables.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
listLength.lean	feat: use simple List.length definition and add csimp theorem	2021-08-21 13:11:06 -07:00
listLength.lean.expected.out	chore: add a new tagged IRType for inline tagged scalars (#9394)	2025-07-16 00:42:56 +00:00
lit_values.lean
lit_values.lean.expected.out
localNotationPP.lean
localNotationPP.lean.expected.out
longestParsePrio.lean
longestParsePrio.lean.expected.out
loopErrorRecovery.lean
loopErrorRecovery.lean.expected.out
lvl1.lean	chore: fix tests	2022-07-02 15:17:01 -07:00
lvl1.lean.expected.out
macroElabRulesIssue1.lean
macroElabRulesIssue1.lean.expected.out
macroElabRulesIssue2.lean
macroElabRulesIssue2.lean.expected.out
macroError.lean
macroError.lean.expected.out
macroPrio.lean
macroPrio.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
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: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
macroSwizzle.lean
macroSwizzle.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
macroTrace.lean
macroTrace.lean.expected.out
mangling.lean
mangling.lean.expected.out
match1.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
match1.lean.expected.out	fix: preserve error locations when expanding match arms (#10783)	2025-10-15 13:31:42 +00:00
match2.lean	feat: ignore {} annotation at constructors	2022-04-13 08:30:21 -07:00
match2.lean.expected.out
match3.lean	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
match3.lean.expected.out
match4.lean	feat: upstream definition of Vector from Batteries (#6197)	2024-11-24 23:01:32 +00:00
match4.lean.expected.out
matchAltIndent.lean
matchAltIndent.lean.expected.out
matchApp.lean
matchApp.lean.expected.out
matchErrorLocation.lean
matchErrorLocation.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
matchErrorMsg.lean
matchErrorMsg.lean.expected.out
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
matchPatternPartialApp.lean.expected.out
matchunit.lean	chore: special support for match d with | PUnit.unit => rhs	2021-02-10 09:54:12 -08:00
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	chore: fix tests	2021-08-07 13:22:58 -07:00
modBug.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
moduleDoc.lean
moduleDoc.lean.expected.out
moduleKeywords.lean	refactor: move import validation to parser & Lake (#9716)	2025-08-05 22:36:54 +00:00
moduleKeywords.lean.expected.out	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
moduleOf.lean
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
mulcommErrorMessage.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
multiConstantError.lean
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
mutualWithNamespaceMacro.lean.expected.out
mutwf1.lean	chore: cleanup #5167 workarounds after update stage0 (#5175)	2024-08-26 17:53:30 +00:00
mutwf1.lean.expected.out
mutwftypemismatch.lean
mutwftypemismatch.lean.expected.out
mvar_fvar.lean
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean
mvarAtDefaultValue.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
nameArgErrorIssue.lean
nameArgErrorIssue.lean.expected.out	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
namedHoles.lean
namedHoles.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
namelit.lean	feat: delab Name.mkStr/Num	2021-05-19 09:21:52 +02:00
namelit.lean.expected.out
nameRepr.lean	fix: Repr Name instance	2021-09-18 15:29:32 -07:00
nameRepr.lean.expected.out
negFloat.lean
negFloat.lean.expected.out
newCatPanic.lean
newCatPanic.lean.expected.out
nonAtomicFieldName.lean
nonAtomicFieldName.lean.expected.out	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
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	refactor: update and consolidate attribute-related error messages (#9495)	2025-07-26 02:03:18 +00:00
nonReserved.lean
nonReserved.lean.expected.out
noTabs.lean	chore: for #8914 after stage0 update, part 2 (#8931)	2025-06-22 22:40:00 +00:00
noTabs.lean.expected.out	chore: for #8914 after stage0 update, part 2 (#8931)	2025-06-22 22:40:00 +00:00
notationDelab.lean	feat: make cdot expansion take hygiene into account (#9443)	2025-07-24 00:43:32 +00:00
notationDelab.lean.expected.out
notationPrecheck.lean
notationPrecheck.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
openExport.lean
openExport.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
openScoped.lean
openScoped.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
optionGetD.lean
optionGetD.lean.expected.out
or_shortcircuit.lean
or_shortcircuit.lean.expected.out
parserPrio.lean
parserPrio.lean.expected.out	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
parserRecovery.lean
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
partial_fixpoint_parseerrors.lean.expected.out
partialIssue.lean
partialIssue.lean.expected.out
partialSyntaxTraces.lean
partialSyntaxTraces.lean.expected.out	feat: allow combining private/public and protected	2025-08-09 12:35:07 +02:00
partialVariable.lean
partialVariable.lean.expected.out
patvar.lean	fix: simple-match macro	2021-01-12 06:41:32 -08:00
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	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
ppBeta.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
ppBeta.lean.expected.out
ppDeepTerms.lean
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	test: pretty printing if-then-else	2020-12-24 08:40:30 -08:00
ppite.lean.expected.out
pplevel.lean	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
pplevel.lean.expected.out
ppMotives.lean	style: replace HEq x y with x ≍ y (#8872)	2025-06-20 07:47:33 +00:00
ppMotives.lean.expected.out
ppNotationCode.lean
ppNotationCode.lean.expected.out	fix: detect private references in inferred type of public def (#10762)	2025-10-15 12:51:54 +00:00
ppProofs.lean
ppProofs.lean.expected.out
PPRoundtrip.lean	refactor: remove Lean.RBMap usages (#9260)	2025-07-21 14:04:45 +00:00
PPRoundtrip.lean.expected.out
ppSyntax.lean
ppSyntax.lean.expected.out
precissues.lean	chore: adapt stdlib & tests	2021-05-20 15:17:36 -07:00
precissues.lean.expected.out
private.lean	fix: let private names be unresolved in the pretty printer, fix shadowing bug when pp.universes is true (#8617)	2025-06-03 23:37:35 +00:00
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
privateFieldCopyIssue.lean.expected.out
Process.lean	test: remove flaky test (#5468)	2024-09-25 08:18:42 +00:00
Process.lean.expected.out
promise.lean	refactor: more complete channel implementation for Std.Channel (#7819)	2025-04-12 21:02:24 +00:00
promise.lean.expected.out
protected.lean
protected.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
protectedAlias.lean
protectedAlias.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
pureCoeIssue.lean
pureCoeIssue.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
rat1.lean	feat: upstream definition of Rat from Batteries (#9957)	2025-08-19 01:58:24 +00:00
rat1.lean.expected.out
rawStringEOF.lean
rawStringEOF.lean.expected.out
readDir.lean	feat: make FilePath a concrete type	2021-05-28 14:19:59 +02:00
readDir.lean.expected.out
reduceArity.lean	chore: reenable subset of new-compiler tests and delete others	2025-06-20 17:29:10 +02:00
reduceArity.lean.expected.out	fix: include ._closed decls in trace.Compiler.result output (#9336)	2025-07-13 02:24:00 +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	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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	fix: apply newlines before and after comments when formatting syntax (#8626)	2025-06-26 19:23:35 +00:00
renameBug.lean
renameBug.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
renameI.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
renameI.lean.expected.out
replaceLocalDeclInstantiateMVars.lean
replaceLocalDeclInstantiateMVars.lean.expected.out
repr.lean	chore: remove >6 month old deprecations (#9640)	2025-08-05 02:29:15 +00:00
repr.lean.expected.out
repr_issue.lean	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
repr_issue.lean.expected.out
resolveGlobalName.lean
resolveGlobalName.lean.expected.out
revertlet.lean
revertlet.lean.expected.out
rewrite.lean	feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences (#2539)	2024-01-03 00:01:40 +00:00
rewrite.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
rfl_simp_thm.lean
rfl_simp_thm.lean.expected.out
root.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
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	fix: run_meta macro (#3334)	2024-02-15 00:12:45 +00:00
run_meta1.lean.expected.out
runSTBug.lean
runSTBug.lean.expected.out
runTacticMustCatchExceptions.lean
runTacticMustCatchExceptions.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
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	feat: use name resolution for dot identifier notation (#9634)	2025-08-01 02:27:40 +00:00
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	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +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	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
scopedunifhint.lean.expected.out
semicolonOrLinebreak.lean
semicolonOrLinebreak.lean.expected.out	feat: add hints for missing structure instance fields (#9317)	2025-07-17 03:22:34 +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	fix: make IO.RealWorld opaque (#9631)	2025-09-08 18:12:19 +00:00
setLit.lean	chore: set literal notation (#3348)	2024-02-19 23:22:36 +00:00
setLit.lean.expected.out	chore: use UTF8 instead of Utf8 in identifiers (#10636)	2025-10-01 17:57:32 +00:00
shadow.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
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	feat: transform nondependent lets into haves in declarations and equation lemmas (#8373)	2025-06-29 19:45:45 +00:00
simp_trace_backtrack.lean
simp_trace_backtrack.lean.expected.out
simpArgTypeMismatch.lean
simpArgTypeMismatch.lean.expected.out	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
simpArrayIdx.lean
simpArrayIdx.lean.expected.out
simpcfg.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
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
simprocEval4.lean.expected.out
simprocTrace.lean
simprocTrace.lean.expected.out
simpTracePostIssue.lean
simpTracePostIssue.lean.expected.out
simpZetaFalse.lean	feat: optimized simp routine for let telescopes (#8968)	2025-06-27 02:13:20 +00:00
simpZetaFalse.lean.expected.out	feat: optimized simp routine for let telescopes (#8968)	2025-06-27 02:13:20 +00:00
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	feat: make #check <ident> always show the signature without elaboration	2022-12-21 21:59:05 +01:00
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	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
sorryWarning.lean
sorryWarning.lean.expected.out
specializeAttr.lean
specializeAttr.lean.expected.out	refactor: update and consolidate attribute-related error messages (#9495)	2025-07-26 02:03:18 +00:00
split_mvars_target.lean
split_mvars_target.lean.expected.out
splitIssue.lean
splitIssue.lean.expected.out
stdio.lean	fix: invalid namespace completions (#5322)	2024-09-13 12:23:03 +00:00
stdio.lean.expected.out	feat: make std streams Streams	2020-08-28 10:04:32 -07:00
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
string_imp.lean.expected.out
string_imp2.lean	feat: redefine String, part one (#10304)	2025-09-18 11:36:52 +00:00
string_imp2.lean.expected.out
struct1.lean	feat: only direct parents of classes create projections (#5920)	2024-11-12 01:55:17 +00:00
struct1.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
structAutoBound.lean
structAutoBound.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
structDefault.lean
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
structInst1.lean.expected.out	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
structInstError.lean
structInstError.lean.expected.out
structInstSourcesLeftToRight.lean
structInstSourcesLeftToRight.lean.expected.out
structSorryBug.lean
structSorryBug.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
StxQuot.lean	feat: parity between structure instance notation and where notation (#6165)	2024-11-30 20:27:25 +00:00
StxQuot.lean.expected.out	chore: minor module system fixes from batteries port (#10496)	2025-09-24 08:59:23 +00:00
substFails.lean	feat: subst notation (heq ▸ h) tries both orientation (#4046)	2024-05-02 07:02:40 +00:00
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	feat: grind internal CommRing class (#7797)	2025-04-03 08:30:19 +00:00
synthorder.lean.expected.out
tabulate.lean
tabulate.lean.expected.out	feat: upstream definition of Vector from Batteries (#6197)	2024-11-24 23:01:32 +00:00
tacUnsolvedGoalsErrors.lean
tacUnsolvedGoalsErrors.lean.expected.out
tcloop.lean	feat: add options maxHeartbeats and synthInstance.maxHeartbeats	2021-01-24 17:45:50 -08:00
tcloop.lean.expected.out	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
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	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
thunk.lean	refactor: clean up Thunk	2021-04-22 20:29:08 -07:00
thunk.lean.expected.out
toExpr.lean	test: toExpr tests	2024-02-23 15:16:12 -08:00
toExpr.lean.expected.out
toFieldNameIssue.lean
toFieldNameIssue.lean.expected.out
tokenErrors.lean
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
traceTacticSteps.lean.expected.out
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	chore: cleanup some deprecations in tests (#5834)	2024-10-25 11:11:22 +00:00
treeMap.lean.expected.out
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	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
typeOf.lean	chore: remove old notation	2021-10-02 15:06:40 -07:00
typeOf.lean.expected.out	feat: prettier expected type mismatch error message (#9099)	2025-07-01 07:50:53 +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
uintMatch.lean.expected.out
unboxStruct.lean
unboxStruct.lean.expected.out	chore: add a new tagged IRType for inline tagged scalars (#9394)	2025-07-16 00:42:56 +00:00
unexpander.lean
unexpander.lean.expected.out
unexpandersNamespaces.lean
unexpandersNamespaces.lean.expected.out
UnexpandSubtype.lean
UnexpandSubtype.lean.expected.out
unfold1.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
unfold1.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
unfoldDefEq.lean
unfoldDefEq.lean.expected.out
unfoldFailure.lean
unfoldFailure.lean.expected.out	refactor: update built-in tactic error messages (#9633)	2025-07-31 14:16:57 +00:00
unfoldReduceMatch.lean
unfoldReduceMatch.lean.expected.out
unhygienic.lean
unhygienic.lean.expected.out
unhygienicCode.lean
unhygienicCode.lean.expected.out	perf: erase all constructor params in the mono phase (#9764)	2025-08-06 14:23:28 +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	feat: update structure/inductive error messages (#9592)	2025-07-29 21:27:30 +00:00
unknownId.lean
unknownId.lean.expected.out	feat: update and explain "unknown constant" and "failed to infer type" errors (#9423)	2025-07-18 19:20:31 +00:00
unknownTactic.lean
unknownTactic.lean.expected.out	chore: for #8914 after stage0 update, part 2 (#8931)	2025-06-22 22:40:00 +00:00
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	feat: transform nondependent lets into haves in declarations and equation lemmas (#8373)	2025-06-29 19:45:45 +00:00
unusedWarningAtStructUpdate.lean
unusedWarningAtStructUpdate.lean.expected.out
updateExprIssue.lean
updateExprIssue.lean.expected.out	fix: populate the xType field of FnBody.case (#9344)	2025-07-13 21:56:07 +00:00
updateLevelIssues.lean
updateLevelIssues.lean.expected.out
Uri.lean	chore: move Bootstrap.System.Uri to Init	2022-08-29 08:06:30 -07: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: add coinductive command to specify coinductive predicates (#10333)	2025-10-07 18:04:51 +00:00
warningAsError.lean
warningAsError.lean.expected.out	feat: note potential discrepancies in deprecation warning (#9606)	2025-07-31 16:41:14 +00:00
wf1.lean	feat: arity mismatch error message at well-founded recursion	2021-09-21 20:34:15 -07:00
wf1.lean.expected.out
wf2.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
wf2.lean.expected.out
wfrecUnusedLet.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
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
withSetOptionIn.lean.expected.out	fix: check guard_msgs.diff using .get rather than Options.getBool (#8918)	2025-06-21 16:03:31 +00:00
workspaceSymbols.lean
workspaceSymbols.lean.expected.out
xmlParsing.lean
xmlParsing.lean.expected.out
zipper.lean	chore: fix tests	2022-01-15 12:18:09 -08:00
zipper.lean.expected.out