lean4-htt

History

Marc Huisinga a58520da16 fix: travelling auto-completion (#5257 ) Fixes #4455, fixes #4705, fixes #5219 Also fixes a minor bug where a dot in brackets would report incorrect completions instead of no completions. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>		2024-09-10 07:26:44 +00:00
..
interactive	fix: travelling auto-completion (#5257 )	2024-09-10 07:26:44 +00:00
new-compiler	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
Reformat
run	chore: rename Array.data to Array.toList	2024-09-10 15:24:23 +10:00
server	fix: make watchdog more resilient against badly behaving clients (#4443 )	2024-06-13 13:48:36 +00:00
trust0
.gitignore
217.lean
217.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
220.lean
220.lean.expected.out
223.lean
223.lean.expected.out
236.lean
236.lean.expected.out
241.lean
241.lean.expected.out
242.lean
242.lean.expected.out
243.lean
243.lean.expected.out	feat: apply `pp_using_anonymous_constructor` attribute (#3735 )	2024-03-22 00:30:36 +00:00
247.lean
247.lean.expected.out
248.lean
248.lean.expected.out
255.lean
255.lean.expected.out
276.lean	fix: make `elabAsElim` aware of explicit motive arguments (#4817 )	2024-07-29 19:18:47 +00:00
276.lean.expected.out	fix: make `elabAsElim` aware of explicit motive arguments (#4817 )	2024-07-29 19:18:47 +00:00
277a.lean
277a.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
277b.lean
277b.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
283.lean
283.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
297.lean
297.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
301.lean
301.lean.expected.out	fix: validate UTF-8 at C++ -> Lean boundary (#3963 )	2024-06-19 14:05:48 +00:00
302.lean
302.lean.expected.out
307.lean
307.lean.expected.out
309.lean
309.lean.expected.out
331.lean
331.lean.expected.out
345.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
346.lean
346.lean.expected.out
348.lean
348.lean.expected.out	feat: PProd syntax (part 3) (#4756 )	2024-07-16 21:06:04 +00:00
353.lean
353.lean.expected.out
361.lean
361.lean.expected.out
366.lean
366.lean.expected.out	chore: use emoji variant of ✅️,❌️,💥️ (#5173 )	2024-08-26 19:46:37 +00:00
386.lean
386.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
389.lean
389.lean.expected.out
414.lean
414.lean.expected.out
415.lean
415.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
421.lean
421.lean.expected.out
423.lean
423.lean.expected.out
435.lean
435.lean.expected.out
435b.lean
435b.lean.expected.out
439.lean.expected.out	feat: add `pp.fieldNotation.generalized` for generalized field notation, add `@[pp_nodot]` attribute (#3737 )	2024-03-22 08:55:02 +00:00
440.lean
440.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
445.lean
445.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
448.lean
448.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
449.lean
449.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
450.lean
450.lean.expected.out
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
474.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
490.lean
490.lean.expected.out
496.lean
496.lean.expected.out
529.lean
529.lean.expected.out
550.lean
550.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
586.lean
586.lean.expected.out
593.lean
593.lean.expected.out
603.lean.expected.out
604.lean
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	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
625.lean
625.lean.expected.out
641.lean
641.lean.expected.out
653.lean
653.lean.expected.out
655.lean
655.lean.expected.out
679.lean
679.lean.expected.out
689.lean
689.lean.expected.out
690.lean
690.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
697.lean
697.lean.expected.out
714.lean
714.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
755.lean
755.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
770.lean
770.lean.expected.out
799.lean
799.lean.expected.out	feat: show signature elaboration errors on body parse error (#4267 )	2024-05-24 10:07:07 +00:00
801.lean
801.lean.expected.out
813.lean
813.lean.expected.out	fix: discrepancy `theorem` vs `example` (#4493 )	2024-06-24 01:18:41 +00:00
815b.lean
815b.lean.expected.out	chore: use emoji variant of ✅️,❌️,💥️ (#5173 )	2024-08-26 19:46:37 +00:00
906.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
906.lean.expected.out	chore: fix tests	2024-05-01 03:19:39 +02:00
916.lean
916.lean.expected.out
948.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +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	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
973.lean
973.lean.expected.out
973b.lean
973b.lean.expected.out	chore: use emoji variant of ✅️,❌️,💥️ (#5173 )	2024-08-26 19:46:37 +00:00
995.lean
995.lean.expected.out
1007.lean
1007.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
1011.lean
1011.lean.expected.out
1018unknowMVarIssue.lean
1018unknowMVarIssue.lean.expected.out	fix: hovers on binders with metavariables (#4192 )	2024-05-21 10:34:58 +00:00
1021.lean
1021.lean.expected.out	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
1027.lean
1027.lean.expected.out
1038.lean
1038.lean.expected.out
1039.lean
1039.lean.expected.out
1050.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1050.lean.expected.out	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1057.lean
1057.lean.expected.out
1062.lean
1062.lean.expected.out
1074b.lean
1074b.lean.expected.out
1079.lean
1079.lean.expected.out	feat: ppOrigin to use MessageData.ofConst (#4362 )	2024-06-05 11:00:34 +00:00
1081.lean
1081.lean.expected.out	feat: apply `pp_using_anonymous_constructor` attribute (#3735 )	2024-03-22 00:30:36 +00:00
1098.lean
1098.lean.expected.out
1102.lean
1102.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
1112.lean
1112.lean.expected.out
1113.lean
1113.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
1163.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
1206.lean
1206.lean.expected.out
1235.lean
1235.lean.expected.out
1240.lean
1240.lean.expected.out
1275.lean
1275.lean.expected.out
1279.lean
1279.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
1279_simplified.lean
1279_simplified.lean.expected.out
1292.lean
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
1301.lean.expected.out
1321.lean
1321.lean.expected.out
1358.lean
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
1367.lean
1367.lean.expected.out
1371.lean
1371.lean.expected.out
1377.lean
1377.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
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	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
1668.lean
1668.lean.expected.out
1673.lean
1673.lean.expected.out	feat: infer mutual structural recursion (#4718 )	2024-07-15 09:34:06 +00:00
1681.lean
1681.lean.expected.out
1682.lean
1682.lean.expected.out	fix: discrepancy `theorem` vs `example` (#4493 )	2024-06-24 01:18:41 +00:00
1690.lean
1690.lean.expected.out	fix: validate UTF-8 at C++ -> Lean boundary (#3963 )	2024-06-19 14:05:48 +00:00
1705.lean
1705.lean.expected.out
1707.lean
1707.lean.expected.out	fix: validate UTF-8 at C++ -> Lean boundary (#3963 )	2024-06-19 14:05:48 +00:00
1719.lean
1719.lean.expected.out
1760.lean
1760.lean.expected.out
1763.lean
1763.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
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	chore: `pp.proofs.withType` is now false by default (#3379 )	2024-02-17 15:09:24 +00:00
1870.lean	chore: reduce usage of refine' (#5042 )	2024-08-14 15:14:44 +00:00
1870.lean.expected.out	chore: reduce usage of refine' (#5042 )	2024-08-14 15:14:44 +00:00
1878.lean
1878.lean.expected.out
1891.lean
1891.lean.expected.out
1918.lean
1918.lean.expected.out
1971.lean
1971.lean.expected.out	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
2005.lean
2005.lean.expected.out
2006.lean
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
2077.lean.expected.out
2115.lean
2115.lean.expected.out
2125.lean
2125.lean.expected.out
2178.lean	fix: fixes #2178 (#2784 )	2023-10-30 15:06:56 +11:00
2178.lean.expected.out	fix: fixes #2178 (#2784 )	2023-10-30 15:06:56 +11:00
2273.lean
2273.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
2361.lean	feat: withAssignableSyntheticOpaque in assumption (#2596 )	2023-10-30 04:00:52 +00:00
2361.lean.expected.out	feat: withAssignableSyntheticOpaque in assumption (#2596 )	2023-10-30 04:00:52 +00:00
2505.lean
2505.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
2514.lean	fix: dsimp missing consumeMData when closing goals by rfl (#2776 )	2023-10-30 09:32:32 +11:00
2514.lean.expected.out	fix: dsimp missing consumeMData when closing goals by rfl (#2776 )	2023-10-30 09:32:32 +11:00
2634.lean	fix: `simp` fails when custom discharger makes no progress (#3317 )	2024-02-17 13:42:04 +00:00
2634.lean.expected.out	fix: `simp` fails when custom discharger makes no progress (#3317 )	2024-02-17 13:42:04 +00:00
3057.lean	fix: manage all declarations in a given derive (#3058 )	2024-01-09 07:42:06 +00:00
3057.lean.expected.out	fix: eta-expanded instances at `SynthInstance.lean` (#3638 )	2024-03-08 20:37:38 +00:00
3140.lean	fix: `derive BEq` on structure with `Prop`-fields (#3191 )	2024-01-18 02:32:51 +00:00
3140.lean.expected.out	fix: `derive BEq` on structure with `Prop`-fields (#3191 )	2024-01-18 02:32:51 +00:00
3989_1.lean	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
3989_1.lean.expected.out	feat: show signature elaboration errors on body parse error (#4267 )	2024-05-24 10:07:07 +00:00
3989_2.lean	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
3989_2.lean.expected.out	feat: show signature elaboration errors on body parse error (#4267 )	2024-05-24 10:07:07 +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	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
4117.lean	fix: add `checkSystem` and `withIncRecDepth` to `withAutoBoundImplicit` (#4128 )	2024-05-10 21:55:26 +00:00
4117.lean.expected.out	fix: add `checkSystem` and `withIncRecDepth` to `withAutoBoundImplicit` (#4128 )	2024-05-10 21:55:26 +00:00
4240.lean	fix: accidental ownership with specialization	2024-06-07 13:59:22 +02:00
4240.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +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	fix: panic when applying `@[simp]` to malformed theorem syntax (#4341 )	2024-06-04 16:52:26 +00:00
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	fix: kernel exception from fvars left from `?m a b` instantiation (#4410 )	2024-06-10 19:02:27 +00:00
4452.lean	fix: `deprecated` warning position at `simp` arguments (#4484 )	2024-06-17 23:21:14 +00:00
4452.lean.expected.out	fix: `deprecated` warning position at `simp` arguments (#4484 )	2024-06-17 23:21:14 +00:00
4591.lean	fix: unresolve name avoiding locals (#4593 )	2024-07-02 01:15:39 +00:00
4591.lean.expected.out	fix: unresolve name avoiding locals (#4593 )	2024-07-02 01:15:39 +00:00
abst.lean
abst.lean.expected.out
allFieldForConstants.lean	chore: upstream Std.Data.List.Init.Lemmas (#3341 )	2024-02-15 03:19:23 +00:00
allFieldForConstants.lean.expected.out
ambiguousOpenExport.lean
ambiguousOpenExport.lean.expected.out
antiquotRecovery.lean
antiquotRecovery.lean.expected.out
appParserIssue.lean
appParserIssue.lean.expected.out
argNameAtPlaceholderError.lean
argNameAtPlaceholderError.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
argNameIfMacroScopes.lean
argNameIfMacroScopes.lean.expected.out
arrayGetU.lean
arrayGetU.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
attrCmd.lean
attrCmd.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
autobound_and_macroscopes.lean
autobound_and_macroscopes.lean.expected.out
autoBoundErrorMsg.lean
autoBoundErrorMsg.lean.expected.out
autoBoundImplicits1.lean
autoBoundImplicits1.lean.expected.out
autoBoundImplicits2.lean
autoBoundImplicits2.lean.expected.out
autoBoundPostponeLoop.lean
autoBoundPostponeLoop.lean.expected.out
autoImplicitChain.lean	feat: add a linter for local vars that clash with their constructors (#4301 )	2024-06-14 13:03:09 +00:00
autoImplicitChain.lean.expected.out
autoImplicitChainNameIssue.lean
autoImplicitChainNameIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
autoImplicitCtorParamIssue.lean
autoImplicitCtorParamIssue.lean.expected.out
autoImplicitForbidden.lean
autoImplicitForbidden.lean.expected.out
autoIssue.lean
autoIssue.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
autoPPExplicit.lean
autoPPExplicit.lean.expected.out	fix: discrepancy in the elaborators for `theorem`, `def`, and `example` (#4482 )	2024-06-27 00:58:58 +00:00
auxDeclIssue.lean
auxDeclIssue.lean.expected.out
badBinderName.lean
badBinderName.lean.expected.out
badIhName.lean
badIhName.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00: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	chore: upstream Std.Util.ExtendedBinders (#3320 )	2024-02-14 11:36:00 +00:00
binderCacheIssue.lean
binderCacheIssue.lean.expected.out
binderCacheIssue2.lean
binderCacheIssue2.lean.expected.out
bindersAbstractingUnassignedMVars.lean
bindersAbstractingUnassignedMVars.lean.expected.out
binop_at_pattern_issue.lean	chore: move `BitVec` to top level namespace	2024-02-23 15:15:57 -08:00
binop_at_pattern_issue.lean.expected.out	fix: match pattern missing test	2024-02-21 05:14:26 -08:00
binop_lazy.lean
binop_lazy.lean.expected.out
binopInfoTree.lean
binopInfoTree.lean.expected.out	fix: don't use info nodes before cursor for completion (#3778 )	2024-04-02 08:49:24 +00:00
binopQuotPrecheck.lean	feat: add `quot_precheck` for expression tree elaborators (`binop%`, etc.) (#3078 )	2023-12-18 16:52:49 +00:00
binopQuotPrecheck.lean.expected.out	feat: add `quot_precheck` for expression tree elaborators (`binop%`, etc.) (#3078 )	2023-12-18 16:52:49 +00:00
binrel_binop.lean
binrel_binop.lean.expected.out	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
binrelTypeMismatch.lean	fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442 )	2024-03-04 00:53:32 +00:00
binrelTypeMismatch.lean.expected.out	fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442 )	2024-03-04 00:53:32 +00:00
binsearch.lean
binsearch.lean.expected.out
bintreeGoal.lean	chore: fix proofs and test	2024-02-09 09:57:57 +11:00
bintreeGoal.lean.expected.out	refactor: move `if-then-else` tactic to `Init`	2024-02-09 09:57:57 +11:00
bitwise.lean
bitwise.lean.expected.out
bool_simp.lean	feat: gaps in Bool lemmas (#5228 )	2024-09-03 04:33:43 +00:00
bool_simp.lean.expected.out	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508 )	2024-03-04 23:56:30 +00:00
builtinSimprocTrace.lean	fix: trace used builtin `simproc`s even if they are not in the environment	2024-01-09 12:57:15 +01:00
builtinSimprocTrace.lean.expected.out	fix: trace used builtin `simproc`s even if they are not in the environment	2024-01-09 12:57:15 +01:00
byCasesMetaM.lean
byCasesMetaM.lean.expected.out
byStrictIndent.lean
byStrictIndent.lean.expected.out
bytearray.lean	fix: toUInt64LE! and toUInt64BE! are swapped (#3660 )	2024-03-28 01:13:42 +00:00
bytearray.lean.expected.out
cacheIssue.lean
cacheIssue.lean.expected.out
calcErrors.lean
calcErrors.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
casesOnCases.lean
casesOnCases.lean.expected.out
caseSuggestions.lean	feat: type of theorems must be propositions	2024-03-13 12:37:58 -07:00
caseSuggestions.lean.expected.out
cdotAtSimpArg.lean	fix: look through binop% variants in `elabCDotFunctionAlias?`	2023-11-12 16:57:51 +11:00
cdotAtSimpArg.lean.expected.out	fix: look through binop% variants in `elabCDotFunctionAlias?`	2023-11-12 16:57:51 +11: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	fix: extended `coe` notation and delaborator (#3295 )	2024-02-10 04:58:28 +00:00
coeAttr1.lean	chore: upstream Std.Tactic.CoeExt to Lean.Elab.CoeExt (#3280 )	2024-02-09 04:55:49 +00:00
coeAttr1.lean.expected.out	chore: upstream Std.Tactic.CoeExt to Lean.Elab.CoeExt (#3280 )	2024-02-09 04:55:49 +00:00
coeM.lean	fix: make `Lean.Internal.liftCoeM` and `Lean.Internal.coeM` unfold (#3404 )	2024-02-27 22:17:46 +00:00
coeM.lean.expected.out	fix: make `Lean.Internal.liftCoeM` and `Lean.Internal.coeM` unfold (#3404 )	2024-02-27 22:17:46 +00:00
collectDepsIssue.lean
collectDepsIssue.lean.expected.out
commandPrefix.lean
commandPrefix.lean.expected.out
computedFieldsCode.lean
computedFieldsCode.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
congrThm.lean
congrThm.lean.expected.out	chore: `pp.proofs.withType` is now false by default (#3379 )	2024-02-17 15:09:24 +00:00
congrThmIssue.lean
congrThmIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
constDelab.lean
constDelab.lean.expected.out
constructorTac.lean
constructorTac.lean.expected.out
consumePPHint.lean
consumePPHint.lean.expected.out
conv1.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
conv1.lean.expected.out	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +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	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternAtLetIssue.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternAtLetIssue.lean.expected.out
convPatternMatchIssue.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternMatchIssue.lean.expected.out
convZetaLetExt.lean
convZetaLetExt.lean.expected.out
copy-produced	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
csimpAttr.lean
csimpAttr.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
csimpAttrAppend.lean
csimpAttrAppend.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
ctor_layout.lean	chore: revert "chore: temporarily remove test broken by #4746 " (#5201 )	2024-08-29 08:47:48 +00:00
ctor_layout.lean.expected.out	chore: revert "chore: temporarily remove test broken by #4746 " (#5201 )	2024-08-29 08:47:48 +00:00
ctorUnivTooBig.lean
ctorUnivTooBig.lean.expected.out
dbgMacros.lean
dbgMacros.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
decEqMutualInductives.lean
decEqMutualInductives.lean.expected.out	refactor: deriving DecidableEq to use `termination_by structural` (#4826 )	2024-07-29 21:24:05 +00:00
decimals.lean
decimals.lean.expected.out
decreasing_by.lean	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
decreasing_by.lean.expected.out	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
defaultInstance.lean
defaultInstance.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
defaultInstanceWithPrio.lean
defaultInstanceWithPrio.lean.expected.out
defInst.lean
defInst.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
delabDoLetFun.lean	feat: delaborate `have` inside `do` blocks (#3116 )	2024-01-02 09:36:39 +00:00
delabDoLetFun.lean.expected.out	feat: delaborate `have` inside `do` blocks (#3116 )	2024-01-02 09:36:39 +00:00
delabOverApp.lean	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabOverApp.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabUnexpand.lean
delabUnexpand.lean.expected.out
delta.lean
delta.lean.expected.out
deltaRedIndPredBelow.lean	fix: missing `whnf` in `mkBelowBinder` and `mkMotiveBinder` (#2991 )	2023-12-01 14:46:09 +00:00
deltaRedIndPredBelow.lean.expected.out	fix: missing `whnf` in `mkBelowBinder` and `mkMotiveBinder` (#2991 )	2023-12-01 14:46:09 +00:00
deprecated.lean	fix: generate deprecation warnings for dot notation (#3969 )	2024-05-09 04:52:09 +00:00
deprecated.lean.expected.out	feat: improve @[deprecated] attr (#3968 )	2024-04-23 17:00:32 +00:00
derivingDecidableEq.lean
derivingDecidableEq.lean.expected.out
derivingHashable.lean
derivingHashable.lean.expected.out
derivingRpcEncoding.lean	feat: bundle of widget improvements (#2964 )	2023-12-21 06:24:33 +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	fix: make cdot anonymous function notation handle ambiguous notation (#4833 )	2024-08-09 21:16:51 +00:00
diamond2.lean
diamond2.lean.expected.out	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
diamond3.lean
diamond3.lean.expected.out	feat: delaboration collapses parent projections (#3326 )	2024-02-14 23:44:48 +00:00
diamond4.lean
diamond4.lean.expected.out
diamond5.lean
diamond5.lean.expected.out
diamond6.lean
diamond6.lean.expected.out
diamond7.lean
diamond7.lean.expected.out
diamond8.lean
diamond8.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
diamond9.lean
diamond9.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
diamond10.lean
diamond10.lean.expected.out
discrTreeIota.lean	chore: upstream eq_iff_true_of_subsingleton (#4689 )	2024-07-08 21:09:33 +00:00
discrTreeIota.lean.expected.out	feat: ppOrigin to use MessageData.ofConst (#4362 )	2024-06-05 11:00:34 +00:00
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	feat: add `cleanupAnnotations` parameter to `forallTelescope` methods (#4180 )	2024-05-15 22:19:07 +00:00
doErrorMsg.lean
doErrorMsg.lean.expected.out
doIfLet.lean
doIfLet.lean.expected.out
doIssue.lean
doIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
doLetLoop.lean
doLetLoop.lean.expected.out
doNotation1.lean
doNotation1.lean.expected.out	fix: correct typo in invalid reassignment error (#5080 )	2024-08-18 08:10:07 +00:00
doSeqRightIssue.lean
doSeqRightIssue.lean.expected.out
doubleReset.lean	fix: double `reset` bug at `ResetReuse` (#4028 )	2024-04-29 23:26:07 +00:00
doubleReset.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
dsimpViaConst.lean	test: ensure `dsimp` can use `rfl` thm constants	2023-10-20 19:06:40 -07:00
dsimpViaConst.lean.expected.out	test: ensure `dsimp` can use `rfl` thm constants	2023-10-20 19:06:40 -07:00
dsimpZetaIssue.lean
dsimpZetaIssue.lean.expected.out
eagerCoeExpansion.lean
eagerCoeExpansion.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
eagerUnfoldingIssue.lean
eagerUnfoldingIssue.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
ellipsisProjIssue.lean
ellipsisProjIssue.lean.expected.out
elseifDoErrorPos.lean
elseifDoErrorPos.lean.expected.out
emptyc.lean
emptyc.lean.expected.out
emptyTypeAscription.lean
emptyTypeAscription.lean.expected.out
eoi.lean
eoi.lean.expected.out
eraseInsts.lean
eraseInsts.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
eraseSimp.lean
eraseSimp.lean.expected.out	feat: simp to still work even if one simp arg does not work (#4177 )	2024-06-03 14:21:31 +00:00
errorOnInductionForNested.lean
errorOnInductionForNested.lean.expected.out
errorRecoveryBug.lean
errorRecoveryBug.lean.expected.out
eta.lean
eta.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
etaReducedMvarAssignments.lean	fix: eta reduce mvar assignments in `isDefEq` (#4387 )	2024-06-18 23:41:40 +00:00
etaReducedMvarAssignments.lean.expected.out	chore: use emoji variant of ✅️,❌️,💥️ (#5173 )	2024-08-26 19:46:37 +00:00
etaStructIssue.lean
etaStructIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
eval_except.lean
eval_except.lean.expected.out
evalCmd.lean
evalCmd.lean.expected.out
evalInstMessage.lean
evalInstMessage.lean.expected.out
evalLeak.lean	fix: `#eval` command was leaking auxiliary declarations into the environment (#3323 )	2024-02-13 21:44:52 +00:00
evalLeak.lean.expected.out	fix: `#eval` command was leaking auxiliary declarations into the environment (#3323 )	2024-02-13 21:44:52 +00:00
evalNone.lean
evalNone.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
evalSorry.lean
evalSorry.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
evalWithMVar.lean
evalWithMVar.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
exactErrorPos.lean
exactErrorPos.lean.expected.out
exceptionalTrace.lean	fix: broken trace tree on elab runtime exception (#3371 )	2024-02-19 11:15:23 +00:00
exceptionalTrace.lean.expected.out	chore: fix tests	2024-05-01 03:19:39 +02:00
exitAfterParseError.lean
exitAfterParseError.lean.expected.out
expandExplicitBinders.lean
expandExplicitBinders.lean.expected.out
extract.lean
extract.lean.expected.out
failTac.lean
failTac.lean.expected.out
file_not_found.lean
file_not_found.lean.expected.out
filePath.lean	fix: update System.FilePath.parent to handle edge cases for absolute paths (#3645 )	2024-03-26 05:09:44 +00:00
filePath.lean.expected.out	fix: update System.FilePath.parent to handle edge cases for absolute paths (#3645 )	2024-03-26 05:09:44 +00:00
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	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
Format.lean
Format.lean.expected.out
formatTerm.lean	fix: trailing whitespace in `location` formatter (#3318 )	2024-02-13 15:53:29 +00:00
formatTerm.lean.expected.out	fix: trailing whitespace in `location` formatter (#3318 )	2024-02-13 15:53:29 +00:00
fun.lean
fun.lean.expected.out
funExpected.lean
funExpected.lean.expected.out
funind_errors.lean	feat: use reserved name infrastructure for functional induction (#3776 )	2024-03-26 22:25:10 +00:00
funind_errors.lean.expected.out	feat: use reserved name infrastructure for functional induction (#3776 )	2024-03-26 22:25:10 +00:00
funind_reserved.lean	fix: check that funind-reserved names are available (#4135 )	2024-05-12 20:39:14 +00:00
funind_reserved.lean.expected.out	fix: check that funind-reserved names are available (#4135 )	2024-05-12 20:39:14 +00:00
funInfoBug.lean
funInfoBug.lean.expected.out
funParen.lean
funParen.lean.expected.out
gcd.lean
gcd.lean.expected.out
getElem.lean	feat: use omega in the get_elem tactic (#3515 )	2024-02-27 18:52:04 +00:00
getElem.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
guessLex.lean	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
guessLex.lean.expected.out	feat: infer mutual structural recursion (#4718 )	2024-07-15 09:34:06 +00:00
guessLexDiff.lean	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
guessLexDiff.lean.expected.out	feat: infer mutual structural recursion (#4718 )	2024-07-15 09:34:06 +00:00
guessLexFailures.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
guessLexFailures.lean.expected.out	fix: structural recursion: do not check for brecOn too early (#4831 )	2024-07-25 15:25:34 +00:00
guessLexTricky.lean	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
guessLexTricky.lean.expected.out	feat: GuessLex: avoid writing `sizeOf` in termination argument when not needed (#3630 )	2024-03-10 22:57:10 +00:00
guessLexTricky2.lean	feat: GuessLex: print inferred termination argument (#3012 )	2023-12-05 09:41:52 +00:00
guessLexTricky2.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
have.lean
have.lean.expected.out
hidingInaccessibleNames.lean
hidingInaccessibleNames.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
holeErrors.lean
holeErrors.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
holes.lean
holes.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
hpow.lean	chore: typos (#4026 )	2024-04-29 14:04:50 +00:00
hpow.lean.expected.out	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
hygienicIntro.lean
hygienicIntro.lean.expected.out
implementedByIssue.lean
implementedByIssue.lean.expected.out
implicitArgumentError.lean	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
implicitArgumentError.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
implicitLambdaIssue.lean
implicitLambdaIssue.lean.expected.out
implicitTypePos.lean
implicitTypePos.lean.expected.out
indimpltarget.lean	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
indimpltarget.lean.expected.out	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
inductionErrors.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940 )	2024-05-22 13:23:30 +00:00
inductionErrors.lean.expected.out	feat: incremental elaboration of definition headers, bodies, and tactics (#3940 )	2024-05-22 13:23:30 +00:00
inductionGen.lean	fix: `checkTargets` check for duplicate target (#3171 )	2024-01-18 09:44:17 +00:00
inductionGen.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
inductionMutual.lean	feat: add a linter for local vars that clash with their constructors (#4301 )	2024-06-14 13:03:09 +00:00
inductionMutual.lean.expected.out
inductive1.lean
inductive1.lean.expected.out
inductiveUnivErrorMsg.lean
inductiveUnivErrorMsg.lean.expected.out
indUsingTerm.lean	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
indUsingTerm.lean.expected.out	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
infoFromFailure.lean
infoFromFailure.lean.expected.out	chore: use emoji variant of ✅️,❌️,💥️ (#5173 )	2024-08-26 19:46:37 +00:00
inlineIssue.lean
inlineIssue.lean.expected.out
inst.lean
inst.lean.expected.out
instance1.lean
instance1.lean.expected.out
int_div_mod.lean	feat: introduce native functions for Int.ediv / Int.emod (#3376 )	2024-02-19 15:04:51 +00:00
int_div_mod.lean.expected.out	feat: introduce native functions for Int.ediv / Int.emod (#3376 )	2024-02-19 15:04:51 +00:00
intModBug.lean
intModBug.lean.expected.out
intNegSucc.lean
intNegSucc.lean.expected.out
introLetBug.lean
introLetBug.lean.expected.out
invalidEnd.lean
invalidEnd.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: detail error message about invalid mutual blocks (#2949 )	2023-12-05 10:50:10 +00:00
invalidNamedArgs.lean
invalidNamedArgs.lean.expected.out
invalidPatternIssue.lean
invalidPatternIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
IRbug.lean
IRbug.lean.expected.out
isDefEqOffsetBug.lean
isDefEqOffsetBug.lean.expected.out
isNoncomputable.lean
isNoncomputable.lean.expected.out
issue2260.lean	fix: improve error message when termination argument is too dependent (#3414 )	2024-02-22 16:39:26 +00:00
issue2260.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
issue2981.lean	test: expand tests/lean/issue2981.lean a bit (#3007 )	2023-12-01 17:52:34 +00:00
issue2981.lean.expected.out	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
issue3232.lean	feat: apply’s error message should show implicit arguments as needed (#3929 )	2024-05-18 06:25:43 +00:00
issue3232.lean.expected.out	feat: apply’s error message should show implicit arguments as needed (#3929 )	2024-05-18 06:25:43 +00:00
jason2.lean
jason2.lean.expected.out	fix: show argument name in implicit argument error (#4426 )	2024-06-14 18:08:42 +00:00
json.lean
json.lean.expected.out
kernelMVarBug.lean
kernelMVarBug.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
keyAttrErase.lean
keyAttrErase.lean.expected.out	chore: upstream norm_cast tactic (#3322 )	2024-02-19 17:49:17 -08:00
lazySeq.lean
lazySeq.lean.expected.out
lcnfTypes.lean
lcnfTypes.lean.expected.out	chore: extend GetElem with getElem! and getElem? (#3694 )	2024-03-28 01:42:00 +00:00
LE.lean
LE.lean.expected.out
lean3RefineBug.lean
lean3RefineBug.lean.expected.out
letArrowOutsideDo.lean
letArrowOutsideDo.lean.expected.out
letFun.lean	feat: encode `let_fun` using a `letFun` function (#2973 )	2023-12-18 09:01:42 +00:00
letFun.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
letPatIssue.lean
letPatIssue.lean.expected.out
letrec1.lean
letrec1.lean.expected.out
letrecErrors.lean
letrecErrors.lean.expected.out
letRecTheorem.lean
letRecTheorem.lean.expected.out
librarySearch.lean	chore: cherry-pick stray test from #3850 (#4509 )	2024-06-20 01:00:45 +00:00
librarySearch.lean.expected.out	chore: port librarySearch tests from std (#3530 )	2024-02-28 17:24:17 +00:00
liftOverLeft.lean
liftOverLeft.lean.expected.out
linterMissingDocs.lean
linterMissingDocs.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
linterSuspiciousUnexpanderPatterns.lean
linterSuspiciousUnexpanderPatterns.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
linterUnusedVariables.lean	perf: rewrite UnusedVariables lint (#3186 )	2024-03-21 12:28:57 +00:00
linterUnusedVariables.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
listLength.lean
listLength.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
lit_values.lean	feat: add helper functions for recognizing builtin literals	2024-02-24 16:08:07 -08:00
lit_values.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
ll_infer_type_bug.lean
ll_infer_type_bug.lean.expected.out
localNotationPP.lean
localNotationPP.lean.expected.out
longestParsePrio.lean
longestParsePrio.lean.expected.out
loopErrorRecovery.lean
loopErrorRecovery.lean.expected.out
lvl1.lean
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
macroResolveName.lean
macroResolveName.lean.expected.out
macroscopes.lean
macroscopes.lean.expected.out
macroStack.lean
macroStack.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
macroSwizzle.lean
macroSwizzle.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
macroTrace.lean
macroTrace.lean.expected.out
magical.lean
magical.lean.expected.out
mangling.lean
mangling.lean.expected.out
match1.lean
match1.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
match2.lean
match2.lean.expected.out
match3.lean
match3.lean.expected.out
match4.lean
match4.lean.expected.out
matchAltIndent.lean
matchAltIndent.lean.expected.out
matchApp.lean
matchApp.lean.expected.out
matchErrorLocation.lean
matchErrorLocation.lean.expected.out
matchErrorMsg.lean
matchErrorMsg.lean.expected.out
matchLeftovers.lean
matchLeftovers.lean.expected.out
matchMissingCasesAsStuckError.lean
matchMissingCasesAsStuckError.lean.expected.out
matchMultAlt.lean	chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579 )	2024-03-13 05:35:52 +00:00
matchMultAlt.lean.expected.out
matchOfNatIssue.lean	chore: change simp default to decide := false (#2722 )	2023-11-02 10:06:38 +11:00
matchOfNatIssue.lean.expected.out	chore: upstream Std.Data.Int.Init modules (#3364 )	2024-02-16 03:58:23 +00:00
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
matchunit.lean
matchunit.lean.expected.out
matchUnknownFVarBug.lean
matchUnknownFVarBug.lean.expected.out
matchVarNames.lean
matchVarNames.lean.expected.out
metaEvalInstMessage.lean
metaEvalInstMessage.lean.expected.out
missingExplicitWithForwardNamedDep.lean
missingExplicitWithForwardNamedDep.lean.expected.out
mkProjStx.lean
mkProjStx.lean.expected.out
modBug.lean
modBug.lean.expected.out
moduleDoc.lean
moduleDoc.lean.expected.out
moduleOf.lean
moduleOf.lean.expected.out
motiveNotTypeCorect.lean	refactor: rewrite: produce simpler proof terms (#3121 )	2024-01-19 07:20:58 +00:00
motiveNotTypeCorect.lean.expected.out	refactor: rewrite: produce simpler proof terms (#3121 )	2024-01-19 07:20:58 +00:00
mulcommErrorMessage.lean
mulcommErrorMessage.lean.expected.out	fix: make `elabTermEnsuringType` respect `errToSorry` when there is a type mismatch (#3633 )	2024-03-09 15:30:47 +00:00
multiConstantError.lean
multiConstantError.lean.expected.out
mutualdef1.lean
mutualdef1.lean.expected.out	feat: show signature elaboration errors on body parse error (#4267 )	2024-05-24 10:07:07 +00:00
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	feat: always run clean_wf, even before decreasing_by (#5016 )	2024-08-15 14:42:15 +00:00
mutwftypemismatch.lean	refactor: ArgsPacker (#3621 )	2024-03-14 14:59:40 +00:00
mutwftypemismatch.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
mvar_fvar.lean
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean
mvarAtDefaultValue.lean.expected.out
nameArgErrorIssue.lean
nameArgErrorIssue.lean.expected.out
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
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
notationPrecheck.lean.expected.out
openExport.lean
openExport.lean.expected.out
openScoped.lean
openScoped.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
optionGetD.lean	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
optionGetD.lean.expected.out	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
or_shortcircuit.lean
or_shortcircuit.lean.expected.out
parserPrio.lean
parserPrio.lean.expected.out
parserRecovery.lean	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
parserRecovery.lean.expected.out	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
partialIssue.lean	feat: propagate `maxHeartbeats` to kernel (#4113 )	2024-05-09 17:44:19 +00:00
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	feat: snapshot trees and language processors (#3014 )	2024-03-14 13:40:08 +00:00
partialVariable.lean
partialVariable.lean.expected.out
patvar.lean
patvar.lean.expected.out
phashmap_inst_coherence.lean
phashmap_inst_coherence.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
ppBeta.lean	feat: `pp.beta` to apply beta reduction when pretty printing (#2864 )	2023-11-24 12:26:31 +00:00
ppBeta.lean.expected.out	feat: `pp.beta` to apply beta reduction when pretty printing (#2864 )	2023-11-24 12:26:31 +00:00
ppDeepTerms.lean	fix: make omission syntax be a builtin syntax (part 2)	2024-02-28 09:23:17 +01:00
ppDeepTerms.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppExpr.lean
ppExpr.lean.expected.out
PPInstances.lean
PPInstances.lean.expected.out
ppite.lean
ppite.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
pplevel.lean
pplevel.lean.expected.out
ppMotives.lean
ppMotives.lean.expected.out	test: update test output following stage0 update (#4815 )	2024-07-23 21:43:38 +00:00
ppNotationCode.lean
ppNotationCode.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppNumericTypes.lean	feat: `pp.numericTypes` option for printing number literals with type ascriptions (#2933 )	2024-02-01 17:23:32 +11:00
ppNumericTypes.lean.expected.out	feat: `pp.numericTypes` option for printing number literals with type ascriptions (#2933 )	2024-02-01 17:23:32 +11:00
ppProofs.lean	feat: have `pp.proofs` use `⋯` for omission (#3241 )	2024-02-15 21:49:41 +00:00
ppProofs.lean.expected.out	fix: discrepancy `theorem` vs `example` (#4493 )	2024-06-24 01:18:41 +00:00
PPRoundtrip.lean
PPRoundtrip.lean.expected.out
ppSyntax.lean
ppSyntax.lean.expected.out
ppUnicode.lean
ppUnicode.lean.expected.out
precissues.lean
precissues.lean.expected.out
printStructure.lean	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
printStructure.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
private.lean
private.lean.expected.out
privateFieldCopyIssue.lean
privateFieldCopyIssue.lean.expected.out
Process.lean	test: unflakify test cases (#4940 )	2024-08-07 09:34:29 +00:00
Process.lean.expected.out	test: unflakify test cases (#4940 )	2024-08-07 09:34:29 +00:00
promise.lean
promise.lean.expected.out
protected.lean
protected.lean.expected.out
protectedAlias.lean
protectedAlias.lean.expected.out
prvCtor.lean
prvCtor.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
prvNameWithMacroScopes.lean
prvNameWithMacroScopes.lean.expected.out
pureCoeIssue.lean
pureCoeIssue.lean.expected.out
rat1.lean
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
readDir.lean.expected.out
reduceBool.lean
reduceBool.lean.expected.out
redundantAlt.lean
redundantAlt.lean.expected.out
ref1.lean
ref1.lean.expected.out
refineFiltersOldMVars.lean
refineFiltersOldMVars.lean.expected.out	fix: cdot parser error message range (#4528 )	2024-06-21 15:06:07 +00:00
refineOccursCheck.lean
refineOccursCheck.lean.expected.out
Reformat.lean
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	fix: add `instantiateMVars` to `replaceLocalDecl` (#2712 )	2023-10-25 10:26:09 +11:00
repr.lean
repr.lean.expected.out
repr_issue.lean
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	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
rfl_simp_thm.lean
rfl_simp_thm.lean.expected.out
root.lean
root.lean.expected.out
run_meta1.lean	fix: `run_meta` macro (#3334 )	2024-02-15 00:12:45 +00:00
run_meta1.lean.expected.out	fix: `run_meta` macro (#3334 )	2024-02-15 00:12:45 +00:00
runSTBug.lean
runSTBug.lean.expected.out
runTacticMustCatchExceptions.lean
runTacticMustCatchExceptions.lean.expected.out	chore: fix typo and incorrect name in doc (#4404 )	2024-06-23 09:06:50 +00:00
rwEqThms.lean
rwEqThms.lean.expected.out	fix: discrepancy `theorem` vs `example` (#4493 )	2024-06-24 01:18:41 +00:00
rwPrioritizesLCtxOverEnv.lean	fix: make `rw [foo]` look in the local context for `foo` before it looks in the environment (#2738 )	2023-10-30 14:08:02 +11:00
rwPrioritizesLCtxOverEnv.lean.expected.out	fix: make `rw [foo]` look in the local context for `foo` before it looks in the environment (#2738 )	2023-10-30 14:08:02 +11:00
rwWithoutOffsetCnstrs.lean
rwWithoutOffsetCnstrs.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
rwWithSynthesizeBug.lean	fix: `rw ... at h` unknown fvar bug (#2728 )	2023-10-25 01:52:19 +00:00
rwWithSynthesizeBug.lean.expected.out	fix: `rw ... at h` unknown fvar bug (#2728 )	2023-10-25 01:52:19 +00:00
safeShadowing.lean
safeShadowing.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out
sanitychecks.lean
sanitychecks.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
scientific.lean
scientific.lean.expected.out	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
scopedInstanceOutsideNamespace.lean
scopedInstanceOutsideNamespace.lean.expected.out
scopedLocalInsts.lean
scopedLocalInsts.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
scopedMacros.lean
scopedMacros.lean.expected.out
scopedTokens.lean
scopedTokens.lean.expected.out
scopedunifhint.lean.expected.out
semicolonOrLinebreak.lean
semicolonOrLinebreak.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
sepByIndentQuot.lean
sepByIndentQuot.lean.expected.out
setLit.lean	chore: set literal notation (#3348 )	2024-02-19 23:22:36 +00:00
setLit.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
shadow.lean
shadow.lean.expected.out	feat: incrementality for careful command macros such as `set_option in theorem`, `theorem foo.bar`, `lemma` (#4364 )	2024-06-05 14:10:38 +00:00
simp_all_duplicateHyps.lean
simp_all_duplicateHyps.lean.expected.out
simp_dsimp.lean
simp_dsimp.lean.expected.out
simp_trace.lean	feat: Nat.add_left_eq_self and relatives (#5104 )	2024-08-21 04:11:57 +00:00
simp_trace.lean.expected.out	feat: allow users to disable `simpCtorEq` simproc (#5167 )	2024-08-26 13:51:21 +00:00
simp_trace_backtrack.lean	chore: upstream basic statements about inequalities (#3366 )	2024-02-16 05:42:38 +00:00
simp_trace_backtrack.lean.expected.out	chore: upstream basic statements about inequalities (#3366 )	2024-02-16 05:42:38 +00:00
simpArgTypeMismatch.lean
simpArgTypeMismatch.lean.expected.out
simpArrayIdx.lean	feat: port check_tactic commands from Std and add test cases (#3532 )	2024-02-28 23:32:54 +00: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	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocChar.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval1.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval1.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval2.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval2.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval3.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval3.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval4.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval4.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
simprocTrace.lean	chore: fix tests	2024-02-01 16:58:54 +11:00
simprocTrace.lean.expected.out	feat: trace `simproc`s	2024-01-09 12:57:15 +01:00
simpTracePostIssue.lean	fix: `simp.trace` missing pre annotation	2024-01-09 12:57:15 +01:00
simpTracePostIssue.lean.expected.out	fix: `simp.trace` missing pre annotation	2024-01-09 12:57:15 +01:00
simpZetaFalse.lean	chore: fix tests	2023-11-09 04:06:30 -08:00
simpZetaFalse.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
sizeof.lean
sizeof.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
smartUnfolding.lean
smartUnfolding.lean.expected.out	feat: better support for reducing `Nat.rec` (#3616 )	2024-03-06 13:28:07 +00:00
smartUnfoldingMatch.lean
smartUnfoldingMatch.lean.expected.out	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
sorryAtError.lean
sorryAtError.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
sorryWarning.lean
sorryWarning.lean.expected.out
specializeAttr.lean
specializeAttr.lean.expected.out
splitIssue.lean
splitIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
stdio.lean
stdio.lean.expected.out
stream.lean
stream.lean.expected.out
strictImplicit.lean
strictImplicit.lean.expected.out
string_gaps_err_newline.lean	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
string_gaps_err_newline.lean.expected.out	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
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
string_imp2.lean.expected.out
struct1.lean	fix: make `elabTermEnsuringType` respect `errToSorry` when there is a type mismatch (#3633 )	2024-03-09 15:30:47 +00:00
struct1.lean.expected.out
structAutoBound.lean
structAutoBound.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
structDefault.lean
structDefault.lean.expected.out
structDefValueOverride.lean
structDefValueOverride.lean.expected.out
structInst1.lean
structInst1.lean.expected.out
structInstError.lean
structInstError.lean.expected.out
structInstExtraEta.lean	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
structInstExtraEta.lean.expected.out	fix: `zetaDelta := false` regression (#3459 )	2024-02-22 19:10:02 +00: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	feat: delaboration collapses parent projections (#3326 )	2024-02-14 23:44:48 +00:00
structSorryBug.lean
structSorryBug.lean.expected.out
StxQuot.lean	feat: quotations for parser aliases (#4307 )	2024-05-30 09:22:22 +00:00
StxQuot.lean.expected.out	feat: quotations for parser aliases (#4307 )	2024-05-30 09:22:22 +00:00
substBadMotive.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
substBadMotive.lean.expected.out
substFails.lean	feat: subst notation (heq ▸ h) tries both orientation (#4046 )	2024-05-02 07:02:40 +00:00
substFails.lean.expected.out	feat: subst notation (heq ▸ h) tries both orientation (#4046 )	2024-05-02 07:02:40 +00:00
substlet.lean
substlet.lean.expected.out
syntaxErrors.lean
syntaxErrors.lean.expected.out
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.expected.out
syntaxPrec.lean
syntaxPrec.lean.expected.out
syntheticHolesAsPatterns.lean
syntheticHolesAsPatterns.lean.expected.out	chore: fix tests output	2023-10-22 06:48:22 -07:00
syntheticOpaqueReadOnly.lean	fix: oversight in isReadOnlyOrSyntheticOpaque (#4206 )	2024-05-18 21:01:31 +00:00
syntheticOpaqueReadOnly.lean.expected.out	feat: show signature elaboration errors on body parse error (#4267 )	2024-05-24 10:07:07 +00:00
synthorder.lean
synthorder.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
tabulate.lean
tabulate.lean.expected.out
tacUnsolvedGoalsErrors.lean
tacUnsolvedGoalsErrors.lean.expected.out	fix: cdot parser error message range (#4528 )	2024-06-21 15:06:07 +00:00
tcloop.lean
tcloop.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
termination_by.lean	feat: termination_by structural (#4542 )	2024-07-01 16:51:30 +00:00
termination_by.lean.expected.out	feat: unnecessary termination_by clauses cause warnings, not errors (#4809 )	2024-07-22 20:52:14 +00:00
termination_by_vars.lean	feat: improve termination_by error messages (#3255 )	2024-02-05 13:13:53 +00:00
termination_by_vars.lean.expected.out	feat: improve termination_by error messages (#3255 )	2024-02-05 13:13:53 +00:00
termination_by_where.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
termination_by_where.lean.expected.out	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
terminationFailure.lean	feat: safer #eval, and #eval! (#4810 )	2024-07-23 15:26:56 +00:00
terminationFailure.lean.expected.out	feat: infer mutual structural recursion (#4718 )	2024-07-15 09:34:06 +00:00
test_extern.lean	feat: improvements to test_extern command (#3075 )	2024-04-24 03:56:16 +00:00
test_extern.lean.expected.out	feat: improvements to test_extern command (#3075 )	2024-04-24 03:56:16 +00:00
test_single.sh
theoremType.lean
theoremType.lean.expected.out
thunk.lean
thunk.lean.expected.out
toExpr.lean	test: `toExpr` tests	2024-02-23 15:16:12 -08:00
toExpr.lean.expected.out	test: `toExpr` tests	2024-02-23 15:16:12 -08:00
toFieldNameIssue.lean
toFieldNameIssue.lean.expected.out	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
tokenErrors.lean
tokenErrors.lean.expected.out
tooManyVarsAtInduction.lean
tooManyVarsAtInduction.lean.expected.out
traceClassScopes.lean
traceClassScopes.lean.expected.out
traceStateBactracking.lean
traceStateBactracking.lean.expected.out
traceTacticSteps.lean
traceTacticSteps.lean.expected.out
trailingComma.lean	feat: allow trailing comma in tuples, lists, and tactics (#2643 )	2023-11-17 13:31:41 +01:00
trailingComma.lean.expected.out	feat: PProd syntax (part 3) (#4756 )	2024-07-16 21:06:04 +00:00
treeMap.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
treeMap.lean.expected.out	fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176 )	2024-01-13 18:02:41 +00:00
typeIncorrectPat.lean
typeIncorrectPat.lean.expected.out
typeMismatch.lean
typeMismatch.lean.expected.out
typeOf.lean
typeOf.lean.expected.out	chore: shorten suggestion about diagnostics (#4882 )	2024-07-31 17:56:43 +00:00
uintCtors.lean
uintCtors.lean.expected.out
uintMatch.lean
uintMatch.lean.expected.out
unboxStruct.lean
unboxStruct.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +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	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unfoldDefEq.lean
unfoldDefEq.lean.expected.out
unfoldFailure.lean
unfoldFailure.lean.expected.out
unfoldReduceMatch.lean
unfoldReduceMatch.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unhygienic.lean
unhygienic.lean.expected.out
unhygienicCode.lean	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
unhygienicCode.lean.expected.out	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
unifHintAndTC.lean
unifHintAndTC.lean.expected.out	fix: make tests be aware of new instance names (#3936 )	2024-04-17 16:14:51 +02:00
univInference.lean
univInference.lean.expected.out	doc: fix typos around inductiveCheckResultingUniverse (#3309 )	2024-02-12 10:11:50 +00:00
unknownId.lean
unknownId.lean.expected.out
unknownTactic.lean
unknownTactic.lean.expected.out
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unsolvedIndCases.lean
unsolvedIndCases.lean.expected.out	feat: custom eliminators for `induction` and `cases` tactics, and beautiful eliminators for `Nat` (#3629 )	2024-03-09 15:31:51 +00:00
unsound.lean
unsound.lean.expected.out
unused_univ.lean
unused_univ.lean.expected.out
unusedLet.lean
unusedLet.lean.expected.out	test: update test output following stage0 update (#4815 )	2024-07-23 21:43:38 +00:00
unusedWarningAtStructUpdate.lean
unusedWarningAtStructUpdate.lean.expected.out
updateExprIssue.lean
updateExprIssue.lean.expected.out	feat: new snapshot architecture on the cmdline (#3106 )	2024-08-05 15:57:42 +00:00
updateLevelIssues.lean
updateLevelIssues.lean.expected.out
Uri.lean
Uri.lean.expected.out
varBinderUpdate.lean
varBinderUpdate.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
warningAsError.lean
warningAsError.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
wf1.lean
wf1.lean.expected.out	feat: infer mutual structural recursion (#4718 )	2024-07-15 09:34:06 +00:00
wf2.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
wf2.lean.expected.out
wfrecUnusedLet.lean	feat: drop support for termination_by' (#3033 )	2023-12-11 17:33:17 +00:00
wfrecUnusedLet.lean.expected.out	feat: well-founded definitions irreducible by default (#4061 )	2024-05-10 06:45:21 +00:00
whnfProj.lean
whnfProj.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
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	fix: typo in `withSetOptionIn` (#3806 )	2024-04-06 18:00:34 +00:00
withSetOptionIn.lean.expected.out	fix: typo in `withSetOptionIn` (#3806 )	2024-04-06 18:00:34 +00:00
workspaceSymbols.lean
workspaceSymbols.lean.expected.out
xmlParsing.lean
xmlParsing.lean.expected.out
zipper.lean
zipper.lean.expected.out