max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean
History
Kim Morrison 449bc31832
chore: adds (failing) grind algebra tests (#8961)
2025-06-24 03:51:39 +00:00
..
grind chore: adds (failing) grind algebra tests (#8961) 2025-06-24 03:51:39 +00:00
interactive feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
Reformat
run feat: move lean-pr-testing-NNNN branches to a fork (#8933) 2025-06-24 03:30:43 +00:00
server
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
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 fix: validate atoms modulo leading and trailing whitespace (#6012) 2024-11-14 10:40:17 +00:00
242.lean.expected.out
243.lean fix: fixes #243 2021-05-03 13:01:16 -07:00
243.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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
255.lean feat: allow hygienic capture of section variables in quotations 2021-01-24 11:46:04 -08:00
255.lean.expected.out
276.lean fix: make elabAsElim aware of explicit motive arguments (#4817) 2024-07-29 19:18:47 +00:00
276.lean.expected.out
277a.lean chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
277a.lean.expected.out
277b.lean fix: do not evaluate code containing sorry 2021-01-26 15:01:53 -08:00
277b.lean.expected.out
283.lean fix: solve method at isLevelDefEq 2021-01-20 08:36:26 -08:00
283.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
297.lean fix: missing checkAssignment at assignToConstFun 2021-01-26 17:33:33 -08:00
297.lean.expected.out
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
307.lean chore: remove deprecated aliases for Int.tdiv and Int.tmod (#6322) 2024-12-08 05:19:42 +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 fix: improve type-as-hole error message (#8262) 2025-05-09 22:49:37 +00:00
345.lean.expected.out
346.lean chore: improve error message 2021-03-16 20:42:38 -07:00
346.lean.expected.out
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
389.lean test: expand test for 389 2021-04-11 20:55:33 -07:00
389.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
435.lean fix: fixes #435 2021-05-02 18:16:57 -07:00
435.lean.expected.out
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
448.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
448.lean.expected.out
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
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 feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +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
593.lean fix: fixes #593 2021-08-02 10:46:12 -07:00
593.lean.expected.out
603.lean.expected.out
604.lean fix: fixes #604 2021-08-04 17:19:17 -07:00
604.lean.expected.out
620.lean fix: fixes #620 2021-08-10 15:06:06 -07:00
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
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
653.lean fix: fixes #653 2021-09-04 18:42:33 -07:00
653.lean.expected.out
655.lean fix: fixes #655 2021-09-07 12:17:28 -07:00
655.lean.expected.out
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 feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +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
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
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
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
815b.lean chore: fix tests 2022-08-15 08:55:25 -07:00
815b.lean.expected.out
906.lean feat: per-function termination hints 2024-01-10 17:27:35 +01:00
906.lean.expected.out
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 fix: behavior of hard line breaks in Format strings (#8457) 2025-05-29 22:10:27 +00:00
995.lean fix: match tactic should not trigger implicit lambdas 2022-02-04 07:55:56 -08:00
995.lean.expected.out
1007.lean
1007.lean.expected.out
1011.lean
1011.lean.expected.out
1021.lean
1021.lean.expected.out feat: make let and have term syntaxes be consistent (#8914) 2025-06-22 04:22:47 +00:00
1027.lean
1027.lean.expected.out
1038.lean
1038.lean.expected.out
1039.lean
1039.lean.expected.out
1050.lean
1050.lean.expected.out
1057.lean
1057.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
1062.lean
1062.lean.expected.out
1074b.lean
1074b.lean.expected.out
1079.lean feat: linter.loopingSimpArgs (#8865) 2025-06-23 07:36:21 +00:00
1079.lean.expected.out feat: linter.loopingSimpArgs (#8865) 2025-06-23 07:36:21 +00:00
1081.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
1081.lean.expected.out feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
1098.lean
1098.lean.expected.out
1102.lean
1102.lean.expected.out
1112.lean
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
1206.lean.expected.out
1235.lean
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
1275.lean.expected.out
1279.lean
1279.lean.expected.out
1279_simplified.lean
1279_simplified.lean.expected.out
1292.lean
1292.lean.expected.out
1298.lean
1298.lean.expected.out
1301.lean
1301.lean.expected.out
1321.lean
1321.lean.expected.out
1358.lean
1358.lean.expected.out
1363.lean
1363.lean.expected.out
1367.lean
1367.lean.expected.out
1371.lean
1371.lean.expected.out
1377.lean
1377.lean.expected.out
1433.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
1433.lean.expected.out feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
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
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
1668.lean.expected.out
1673.lean
1673.lean.expected.out
1681.lean
1681.lean.expected.out
1682.lean
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
1705.lean.expected.out feat: allow structures to have non-bracketed binders (#8671) 2025-06-17 17:40:18 +00:00
1707.lean
1707.lean.expected.out
1719.lean
1719.lean.expected.out
1760.lean
1760.lean.expected.out
1763.lean
1763.lean.expected.out
1779.lean
1779.lean.expected.out
1781.lean
1781.lean.expected.out
1804.lean
1804.lean.expected.out
1825.lean
1825.lean.expected.out
1845.lean
1845.lean.expected.out
1856.lean
1856.lean.expected.out
1878.lean
1878.lean.expected.out
1891.lean
1891.lean.expected.out
1918.lean
1918.lean.expected.out
1971.lean
1971.lean.expected.out
2005.lean
2005.lean.expected.out
2006.lean
2006.lean.expected.out
2045.lean
2045.lean.expected.out
2077.lean
2077.lean.expected.out
2115.lean
2115.lean.expected.out
2125.lean
2125.lean.expected.out
2178.lean
2178.lean.expected.out
2273.lean
2273.lean.expected.out
2361.lean
2361.lean.expected.out
2505.lean
2505.lean.expected.out
2514.lean
2514.lean.expected.out
2634.lean
2634.lean.expected.out
3057.lean
3057.lean.expected.out
3140.lean
3140.lean.expected.out
3989_1.lean
3989_1.lean.expected.out
3989_2.lean
3989_2.lean.expected.out
4089.lean
4089.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
4117.lean
4117.lean.expected.out
4240.lean
4240.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
4309.lean
4309.lean.expected.out
4375.lean
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
4591.lean.expected.out
4845.lean
4845.lean.expected.out
6601.lean
6601.lean.expected.out
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
antiquotRecovery.lean
antiquotRecovery.lean.expected.out
appParserIssue.lean
appParserIssue.lean.expected.out
argNameAtPlaceholderError.lean
argNameAtPlaceholderError.lean.expected.out
argNameIfMacroScopes.lean
argNameIfMacroScopes.lean.expected.out
arrayGetU.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +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
autobound_and_macroscopes.lean
autobound_and_macroscopes.lean.expected.out
autoBoundErrorMsg.lean
autoBoundErrorMsg.lean.expected.out
autoBoundImplicits1.lean fix: replace bad simp lemmas for Id (#7352) 2025-05-22 22:45:35 +00:00
autoBoundImplicits1.lean.expected.out
autoBoundImplicits2.lean
autoBoundImplicits2.lean.expected.out
autoBoundPostponeLoop.lean
autoBoundPostponeLoop.lean.expected.out
autoImplicitChain.lean
autoImplicitChain.lean.expected.out
autoImplicitChainNameIssue.lean
autoImplicitChainNameIssue.lean.expected.out feat: accurate binder names in signatures (like in output of #check) (#5827) 2024-10-29 16:43:11 +00:00
autoImplicitCtorParamIssue.lean
autoImplicitCtorParamIssue.lean.expected.out
autoImplicitForbidden.lean
autoImplicitForbidden.lean.expected.out
autoIssue.lean feat: structure instance notation elaboration improvements (#7717) 2025-03-30 17:40:36 +00:00
autoIssue.lean.expected.out
autoPPExplicit.lean
autoPPExplicit.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
auxDeclIssue.lean
auxDeclIssue.lean.expected.out
badBinderName.lean
badBinderName.lean.expected.out
badIhName.lean refactor: use Lean version 2021-05-03 10:06:20 -07:00
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 chore: reenable subset of new-compiler tests and delete others 2025-06-20 17:29:10 +02:00
beginEndAsMacro.lean
beginEndAsMacro.lean.expected.out
bigUnivOffsets.lean
bigUnivOffsets.lean.expected.out
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 feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
binop_lazy.lean fix: lazy_binop + coercion bug 2023-07-01 06:05:25 -07:00
binop_lazy.lean.expected.out
binopInfoTree.lean
binopInfoTree.lean.expected.out feat: signature help (#8511) 2025-06-03 17:26:33 +00:00
binopQuotPrecheck.lean
binopQuotPrecheck.lean.expected.out
binrel_binop.lean
binrel_binop.lean.expected.out
binrelTypeMismatch.lean
binrelTypeMismatch.lean.expected.out fix: normalize imax 1 u to u (#7631) 2025-05-21 20:27:53 +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 chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
bool_simp.lean.expected.out
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 style: replace HEq x y with x ≍ y (#8872) 2025-06-20 07:47:33 +00:00
casesOnCases.lean
casesOnCases.lean.expected.out
caseSuggestions.lean
caseSuggestions.lean.expected.out
cdotTuple.lean chore: style use · instead of . for lambda dot notation 2022-03-11 07:49:03 -08:00
cdotTuple.lean.expected.out
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 fix: make sure monad lift coercion elaborator has no side effects (#6024) 2024-11-13 16:22:31 +00:00
coeM.lean.expected.out
collectDepsIssue.lean
collectDepsIssue.lean.expected.out
commandPrefix.lean
commandPrefix.lean.expected.out feat: pretty print letFun using have syntax (#8372) 2025-05-16 15:10:01 +00:00
computedFieldsCode.lean
computedFieldsCode.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
congrThm.lean feat: avoid [Decidable p] instance implicit parameters in congruence theorems when possible 2022-08-02 04:47:42 -07:00
congrThm.lean.expected.out
congrThmIssue.lean
congrThmIssue.lean.expected.out
constDelab.lean
constDelab.lean.expected.out
constructorTac.lean
constructorTac.lean.expected.out
consumePPHint.lean
consumePPHint.lean.expected.out feat: pretty print letFun using have syntax (#8372) 2025-05-16 15:10:01 +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
convInConv.lean
convInConv.lean.expected.out
convPatternAtLetIssue.lean
convPatternAtLetIssue.lean.expected.out
convPatternMatchIssue.lean
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 feat: apply csimp attribute constant replacements 2021-08-21 12:22:15 -07:00
csimpAttr.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
csimpAttrAppend.lean
csimpAttrAppend.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
ctor_layout.lean
ctor_layout.lean.expected.out feat: module header keyword for enabling module system 2025-04-21 18:40:11 +02:00
ctorUnivTooBig.lean
ctorUnivTooBig.lean.expected.out
dbgMacros.lean chore: fix tests 2021-03-11 11:35:51 -08:00
dbgMacros.lean.expected.out
decEqMutualInductives.lean
decEqMutualInductives.lean.expected.out feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
decimals.lean chore: add more decimals tests 2021-10-26 11:51:30 -07:00
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
defaultInstanceWithPrio.lean
defaultInstanceWithPrio.lean.expected.out
defInst.lean feat: improve #eval command 2022-03-12 19:55:15 -08:00
defInst.lean.expected.out
delabDoLetFun.lean
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
deltaRedIndPredBelow.lean
deltaRedIndPredBelow.lean.expected.out
deprecated.lean
deprecated.lean.expected.out
derivingDecidableEq.lean
derivingDecidableEq.lean.expected.out
derivingHashable.lean
derivingHashable.lean.expected.out
derivingRpcEncoding.lean feat: reusable rpc refs (#8105) 2025-06-03 12:35:12 +00:00
derivingRpcEncoding.lean.expected.out
diamond1.lean chore: style use · instead of . for lambda dot notation 2022-03-11 07:49:03 -08:00
diamond1.lean.expected.out
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
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 fix: behavior of hard line breaks in Format strings (#8457) 2025-05-29 22:10:27 +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 fix: make sure local instance detection sees through reductions (#8903) 2025-06-21 06:26:32 +00:00
docstringLinkValidation.lean
docstringLinkValidation.lean.expected.out feat: pre-stage0 groundwork for named error messages (#8649) 2025-06-11 14:52:08 +00:00
doErrorMsg.lean
doErrorMsg.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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 fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
doLetLoop.lean fix: ensure ill-formed if do-statements do not trigger non termination 2021-04-13 15:51:20 -07:00
doLetLoop.lean.expected.out
doNotation1.lean
doNotation1.lean.expected.out
doSeqRightIssue.lean style: replace HEq x y with x ≍ y (#8872) 2025-06-20 07:47:33 +00:00
doSeqRightIssue.lean.expected.out style: replace HEq x y with x ≍ y (#8872) 2025-06-20 07:47:33 +00:00
doubleReset.lean
doubleReset.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
dsimpViaConst.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
dsimpViaConst.lean.expected.out
dsimpZetaIssue.lean
dsimpZetaIssue.lean.expected.out
eagerCoeExpansion.lean
eagerCoeExpansion.lean.expected.out
eagerUnfoldingIssue.lean
eagerUnfoldingIssue.lean.expected.out
ellipsisProjIssue.lean
ellipsisProjIssue.lean.expected.out
elseifDoErrorPos.lean
elseifDoErrorPos.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
emptyc.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
emptyc.lean.expected.out
emptyTypeAscription.lean
emptyTypeAscription.lean.expected.out feat: empty type ascription syntax (e :) (part 2) 2022-11-07 19:10:56 +01: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
eraseSimp.lean feat: enable failIfUnchanged by default in simp 2023-08-16 10:14:23 -07:00
eraseSimp.lean.expected.out
errorOnInductionForNested.lean
errorOnInductionForNested.lean.expected.out
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 feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
etaStructIssue.lean.expected.out feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +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
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
evalNone.lean feat: report errors an unassigned metavars at #eval 2022-06-29 11:53:33 -07:00
evalNone.lean.expected.out
evalSorry.lean fix: do not evaluate code containing sorry 2021-01-26 15:01:53 -08:00
evalSorry.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
evalWithMVar.lean
evalWithMVar.lean.expected.out
exactErrorPos.lean
exactErrorPos.lean.expected.out
exceptionalTrace.lean
exceptionalTrace.lean.expected.out fix: behavior of hard line breaks in Format strings (#8457) 2025-05-29 22:10:27 +00:00
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
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
fixedIndexToParamIssue.lean
fixedIndexToParamIssue.lean.expected.out
fixedIndicesToParams.lean
fixedIndicesToParams.lean.expected.out
forallMetaBounded.lean
forallMetaBounded.lean.expected.out
forErrors.lean test: add test for "broken for" 2020-12-25 10:03:42 -08:00
forErrors.lean.expected.out
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 refactor: avoid nested sequence in simpleBinder 2022-07-08 19:06:10 +02:00
funExpected.lean
funExpected.lean.expected.out
funind_errors.lean
funind_errors.lean.expected.out
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 feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
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 refactor: TerminationArgument → TerminationMeasure (#6727) 2025-01-23 10:41:38 +00:00
guessLex.lean.expected.out
guessLexDiff.lean
guessLexDiff.lean.expected.out fix: GuessLex: also look for negations of Nat comparisons (#8321) 2025-05-13 15:10:19 +00:00
guessLexFailures.lean
guessLexFailures.lean.expected.out
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
hidingInaccessibleNames.lean
hidingInaccessibleNames.lean.expected.out
holeErrors.lean
holeErrors.lean.expected.out fix: improve type-as-hole error message (#8262) 2025-05-09 22:49:37 +00:00
holes.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
holes.lean.expected.out feat: use omission dots for hidden let values in Infoview (#8041) 2025-05-27 23:09:11 +00:00
hpow.lean feat: add date and time functionality (#4904) 2024-11-14 14:04:19 +00:00
hpow.lean.expected.out
hygienicIntro.lean
hygienicIntro.lean.expected.out
implementedByIssue.lean
implementedByIssue.lean.expected.out
implicitArgumentError.lean
implicitArgumentError.lean.expected.out
implicitLambdaIssue.lean
implicitLambdaIssue.lean.expected.out
implicitTypePos.lean
implicitTypePos.lean.expected.out
indimpltarget.lean
indimpltarget.lean.expected.out
inductionErrors.lean
inductionErrors.lean.expected.out feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
inductionGen.lean
inductionGen.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
inductionMutual.lean
inductionMutual.lean.expected.out
inductionParse.lean
inductionParse.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
inductive1.lean
inductive1.lean.expected.out feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
inductiveUnivErrorMsg.lean
inductiveUnivErrorMsg.lean.expected.out
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
int_div_mod.lean
int_div_mod.lean.expected.out
intModBug.lean test: test for Int.mod bug 2021-01-31 08:57:41 -08:00
intModBug.lean.expected.out
intNegSucc.lean
intNegSucc.lean.expected.out
introLetBug.lean
introLetBug.lean.expected.out
invalidFieldName.lean
invalidFieldName.lean.expected.out
invalidInstImplicit.lean
invalidInstImplicit.lean.expected.out
invalidMutualError.lean
invalidMutualError.lean.expected.out
invalidNamedArgs.lean
invalidNamedArgs.lean.expected.out
invalidPatternIssue.lean
invalidPatternIssue.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
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 feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
isDefEqOffsetBug.lean.expected.out feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
isNoncomputable.lean
isNoncomputable.lean.expected.out
issue2260.lean
issue2260.lean.expected.out
issue2981.lean
issue2981.lean.expected.out
issue3232.lean feat: consider universes and projections in addPPExplicitToExposeDiff (#8271) 2025-05-09 15:07:50 +00:00
issue3232.lean.expected.out feat: consider universes and projections in addPPExplicitToExposeDiff (#8271) 2025-05-09 15:07:50 +00:00
jason2.lean fix: missing error messages 2021-03-05 17:20:04 -08:00
jason2.lean.expected.out
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 chore: reenable subset of new-compiler tests and delete others 2025-06-20 17:29:10 +02:00
json.lean
json.lean.expected.out
kernelMVarBug.lean
kernelMVarBug.lean.expected.out
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 chore: remove the old Lean.Data.HashMap implementation (#7519) 2025-03-20 23:49:55 +00:00
lcnfTypes.lean.expected.out fix: use lcAny in more cases of type erasure (#7990) 2025-04-16 22:53:18 +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
letrecErrors.lean
letrecErrors.lean.expected.out
letRecTheorem.lean
letRecTheorem.lean.expected.out
librarySearch.lean feat: do not report metaprogramming declarations via exact? and rw? (#6672) 2025-06-16 09:20:49 +00:00
librarySearch.lean.expected.out feat: do not report metaprogramming declarations via exact? and rw? (#6672) 2025-06-16 09:20:49 +00:00
liftOverLeft.lean
liftOverLeft.lean.expected.out
linterMissingDocs.lean
linterMissingDocs.lean.expected.out
linterSuspiciousUnexpanderPatterns.lean
linterSuspiciousUnexpanderPatterns.lean.expected.out
linterUnusedVariables.lean feat: linter.unusedSimpArgs (#8901) 2025-06-22 09:10:21 +00:00
linterUnusedVariables.lean.expected.out feat: linter.unusedSimpArgs (#8901) 2025-06-22 09:10:21 +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: update expected test outputs 2025-06-20 17:29:10 +02: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
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 feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
macroPrio.lean.expected.out
macroResolveName.lean
macroResolveName.lean.expected.out
macroscopes.lean
macroscopes.lean.expected.out
macroStack.lean
macroStack.lean.expected.out
macroSwizzle.lean
macroSwizzle.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
macroTrace.lean
macroTrace.lean.expected.out
magical.lean fix: reject projection (_ : ∃ x, p).2 2022-03-01 09:00:46 -08:00
magical.lean.expected.out
mangling.lean fix: 32-bit Unicode name mangling 2021-06-23 00:08:20 -07:00
mangling.lean.expected.out
match1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
match1.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
match2.lean feat: ignore {} annotation at constructors 2022-04-13 08:30:21 -07:00
match2.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
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 feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
matchApp.lean.expected.out
matchErrorLocation.lean
matchErrorLocation.lean.expected.out
matchErrorMsg.lean
matchErrorMsg.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
matchLeftovers.lean
matchLeftovers.lean.expected.out
matchMissingCasesAsStuckError.lean
matchMissingCasesAsStuckError.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
matchMultAlt.lean
matchMultAlt.lean.expected.out
matchOfNatIssue.lean
matchOfNatIssue.lean.expected.out
matchOrIssue.lean
matchOrIssue.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
matchPatternInsideBinders.lean
matchPatternInsideBinders.lean.expected.out
matchPatternPartialApp.lean
matchPatternPartialApp.lean.expected.out
matchunit.lean
matchunit.lean.expected.out
matchUnknownFVarBug.lean
matchUnknownFVarBug.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
matchVarNames.lean
matchVarNames.lean.expected.out
metaEvalInstMessage.lean
metaEvalInstMessage.lean.expected.out
modBug.lean chore: fix tests 2021-08-07 13:22:58 -07:00
modBug.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
moduleDoc.lean feat: add position to mod doc 2022-02-16 13:50:19 -08:00
moduleDoc.lean.expected.out
moduleOf.lean chore: remove the old Lean.Data.HashMap implementation (#7519) 2025-03-20 23:49:55 +00:00
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 fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
mulcommErrorMessage.lean
mulcommErrorMessage.lean.expected.out
multiConstantError.lean
multiConstantError.lean.expected.out fix: improve type-as-hole error message (#8262) 2025-05-09 22:49:37 +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 chore: fix tests 2021-09-07 19:14:30 -07:00
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean
mvarAtDefaultValue.lean.expected.out feat: use omission dots for hidden let values in Infoview (#8041) 2025-05-27 23:09:11 +00:00
nameArgErrorIssue.lean
nameArgErrorIssue.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
namedHoles.lean
namedHoles.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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 fix: Repr Name instance 2021-09-18 15:29:32 -07:00
negFloat.lean fix: defaultInstance priorities for Neg Int and OfScientific Float 2021-01-25 13:21:07 -08:00
negFloat.lean.expected.out
newCatPanic.lean
newCatPanic.lean.expected.out
nonAtomicFieldName.lean
nonAtomicFieldName.lean.expected.out
noncompSection.lean
noncompSection.lean.expected.out feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
nondepArrow.lean
nondepArrow.lean.expected.out
nonfatalattrs.lean
nonfatalattrs.lean.expected.out
nonReserved.lean
nonReserved.lean.expected.out
noTabs.lean 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
notationDelab.lean.expected.out
notationPrecheck.lean
notationPrecheck.lean.expected.out
openExport.lean
openExport.lean.expected.out
openScoped.lean
openScoped.lean.expected.out
optionGetD.lean
optionGetD.lean.expected.out
or_shortcircuit.lean
or_shortcircuit.lean.expected.out
parserPrio.lean
parserPrio.lean.expected.out
parserRecovery.lean
parserRecovery.lean.expected.out
partial_fixpoint_parseerrors.lean
partial_fixpoint_parseerrors.lean.expected.out
partialIssue.lean
partialIssue.lean.expected.out
partialSyntaxTraces.lean
partialSyntaxTraces.lean.expected.out
partialVariable.lean
partialVariable.lean.expected.out
patvar.lean fix: simple-match macro 2021-01-12 06:41:32 -08:00
patvar.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
phashmap_inst_coherence.lean
phashmap_inst_coherence.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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: pretty print letFun using have syntax (#8372) 2025-05-16 15:10:01 +00:00
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 chore: notation for HEq (#8503) 2025-05-27 19:22:57 +00:00
ppNotationCode.lean
ppNotationCode.lean.expected.out feat: pretty print letFun using have syntax (#8372) 2025-05-16 15:10:01 +00:00
ppProofs.lean feat: have pp.proofs use ⋯ for omission (#3241) 2024-02-15 21:49:41 +00:00
ppProofs.lean.expected.out
PPRoundtrip.lean
PPRoundtrip.lean.expected.out
ppSyntax.lean feat: strengthen pp* signatures 2022-07-03 19:14:49 +02:00
ppSyntax.lean.expected.out
ppUnicode.lean feat: add fun x ↦ y syntax 2023-01-03 13:59:53 -08:00
ppUnicode.lean.expected.out
precissues.lean
precissues.lean.expected.out feat: pretty print letFun using have syntax (#8372) 2025-05-16 15:10:01 +00:00
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: 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
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
protectedAlias.lean
protectedAlias.lean.expected.out
prvNameWithMacroScopes.lean
prvNameWithMacroScopes.lean.expected.out
pureCoeIssue.lean
pureCoeIssue.lean.expected.out
rat1.lean feat: add date and time functionality (#4904) 2024-11-14 14:04:19 +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 chore: reenable subset of new-compiler tests and delete others 2025-06-20 17:29:10 +02:00
reduceBool.lean
reduceBool.lean.expected.out
redundantAlt.lean
redundantAlt.lean.expected.out feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
ref1.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
ref1.lean.expected.out
refineFiltersOldMVars.lean
refineFiltersOldMVars.lean.expected.out
refineOccursCheck.lean
refineOccursCheck.lean.expected.out
Reformat.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
Reformat.lean.expected.out
renameBug.lean fix: nasty bug at rename tactic 2021-08-25 15:27:29 -07:00
renameBug.lean.expected.out
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 feat: add helper class ReprAtom 2020-12-18 14:14:46 -08:00
repr.lean.expected.out
repr_issue.lean chore: remove $. notation 2020-11-19 08:47:35 -08: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
rfl_simp_thm.lean
rfl_simp_thm.lean.expected.out feat: track rfl simp theorems 2022-04-21 13:42:04 -07:00
root.lean feat: enable failIfUnchanged by default in simp 2023-08-16 10:14:23 -07:00
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
runSTBug.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
runSTBug.lean.expected.out
runTacticMustCatchExceptions.lean
runTacticMustCatchExceptions.lean.expected.out
rwEqThms.lean feat: allow rw to unfold nonrecursive definitions too 2022-03-12 15:44:52 -08:00
rwEqThms.lean.expected.out
rwPrioritizesLCtxOverEnv.lean
rwPrioritizesLCtxOverEnv.lean.expected.out
rwWithoutOffsetCnstrs.lean
rwWithoutOffsetCnstrs.lean.expected.out
rwWithSynthesizeBug.lean
rwWithSynthesizeBug.lean.expected.out
safeShadowing.lean
safeShadowing.lean.expected.out
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out
sanitychecks.lean
sanitychecks.lean.expected.out
scientific.lean
scientific.lean.expected.out fix: unknown identifier ranges (#8362) 2025-05-22 10:05:31 +00:00
scopedInstanceOutsideNamespace.lean
scopedInstanceOutsideNamespace.lean.expected.out
scopedLocalInsts.lean
scopedLocalInsts.lean.expected.out
scopedMacros.lean
scopedMacros.lean.expected.out
scopedTokens.lean
scopedTokens.lean.expected.out
scopedunifhint.lean.expected.out
semicolonOrLinebreak.lean
semicolonOrLinebreak.lean.expected.out
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 chore: reenable subset of new-compiler tests and delete others 2025-06-20 17:29:10 +02:00
setLit.lean chore: set literal notation (#3348) 2024-02-19 23:22:36 +00:00
setLit.lean.expected.out
shadow.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
shadow.lean.expected.out
simp_all_duplicateHyps.lean
simp_all_duplicateHyps.lean.expected.out
simp_dsimp.lean feat: enable failIfUnchanged by default in simp 2023-08-16 10:14:23 -07:00
simp_dsimp.lean.expected.out
simp_trace.lean chore: upstream Nat material from mathlib (#7971) 2025-04-16 06:55:32 +00:00
simp_trace.lean.expected.out fix: behavior of hard line breaks in Format strings (#8457) 2025-05-29 22:10:27 +00:00
simp_trace_backtrack.lean
simp_trace_backtrack.lean.expected.out
simpArgTypeMismatch.lean
simpArgTypeMismatch.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +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 chore: fix tests 2022-06-14 16:43:22 -07:00
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
simpZetaFalse.lean.expected.out feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804) 2025-06-22 21:54:57 +00:00
sint_basic.lean feat: IntX.ofBitVec (#7048) 2025-02-12 14:49:31 +00:00
sint_basic.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02: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
smartUnfolding.lean
smartUnfolding.lean.expected.out
smartUnfoldingMatch.lean
smartUnfoldingMatch.lean.expected.out
sorryAtError.lean
sorryAtError.lean.expected.out fix: reduce ambiguity of "final" in application type mismatch message (#8322) 2025-05-14 16:12:10 +00:00
sorryWarning.lean
sorryWarning.lean.expected.out
specializeAttr.lean
specializeAttr.lean.expected.out
split_mvars_target.lean fix: Make split work with metavariables in the target (#8437) 2025-05-23 12:46:27 +00:00
split_mvars_target.lean.expected.out fix: Make split work with metavariables in the target (#8437) 2025-05-23 12:46:27 +00:00
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
stream.lean chore: use polymorphic method forIn 2021-02-04 18:13:01 -08:00
stream.lean.expected.out
strictImplicit.lean
strictImplicit.lean.expected.out
string_gaps_err_newline.lean
string_gaps_err_newline.lean.expected.out
string_imp.lean fix: String.splitOn bug (#3832) 2024-04-04 09:30:53 +00:00
string_imp.lean.expected.out
string_imp2.lean
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
structAutoBound.lean
structAutoBound.lean.expected.out
structDefault.lean
structDefault.lean.expected.out
structDefValueOverride.lean
structDefValueOverride.lean.expected.out
structInst1.lean
structInst1.lean.expected.out
structInstError.lean
structInstError.lean.expected.out
structInstSourcesLeftToRight.lean
structInstSourcesLeftToRight.lean.expected.out
structSorryBug.lean
structSorryBug.lean.expected.out
StxQuot.lean feat: parity between structure instance notation and where notation (#6165) 2024-11-30 20:27:25 +00:00
StxQuot.lean.expected.out feat: := private instance syntax 2025-05-28 10:18:04 +02:00
substFails.lean
substFails.lean.expected.out
syntaxErrors.lean
syntaxErrors.lean.expected.out
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.expected.out
syntaxPrec.lean
syntaxPrec.lean.expected.out feat: meta phase restrictions 2025-06-12 16:36:08 +02:00
syntheticHolesAsPatterns.lean
syntheticHolesAsPatterns.lean.expected.out
syntheticOpaqueReadOnly.lean fix: oversight in isReadOnlyOrSyntheticOpaque (#4206) 2024-05-18 21:01:31 +00:00
syntheticOpaqueReadOnly.lean.expected.out
synthorder.lean
synthorder.lean.expected.out
tabulate.lean feat: upstream definition of Vector from Batteries (#6197) 2024-11-24 23:01:32 +00:00
tabulate.lean.expected.out
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
termination_by.lean feat: add support for lattice-theoretic (co)inductive predicates (#8097) 2025-04-30 15:48:58 +00:00
termination_by.lean.expected.out feat: add support for lattice-theoretic (co)inductive predicates (#8097) 2025-04-30 15:48:58 +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 fix: behavior of hard line breaks in Format strings (#8457) 2025-05-29 22:10:27 +00:00
test_single.sh chore: allow module in tests (#8881) 2025-06-21 02:49:22 +00:00
theoremType.lean
theoremType.lean.expected.out fix: improve type-as-hole error message (#8262) 2025-05-09 22:49:37 +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 feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
traceClassScopes.lean
traceClassScopes.lean.expected.out
traceStateBactracking.lean
traceStateBactracking.lean.expected.out
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 feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
typeMismatch.lean
typeMismatch.lean.expected.out
typeOf.lean chore: remove old notation 2021-10-02 15:06:40 -07:00
typeOf.lean.expected.out
uintCtors.lean refactor: redefine unsigned fixed width integers in terms of BitVec (#5323) 2024-10-16 07:28:23 +00:00
uintCtors.lean.expected.out
uintMatch.lean fix: pattern matching on UInt 2021-09-05 19:15:59 -07:00
uintMatch.lean.expected.out
unboxStruct.lean
unboxStruct.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02: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
unfoldDefEq.lean
unfoldDefEq.lean.expected.out
unfoldFailure.lean
unfoldFailure.lean.expected.out
unfoldReduceMatch.lean
unfoldReduceMatch.lean.expected.out
unhygienic.lean
unhygienic.lean.expected.out
unhygienicCode.lean
unhygienicCode.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02:00
unifHintAndTC.lean
unifHintAndTC.lean.expected.out
univInference.lean
univInference.lean.expected.out
unknownId.lean fix: avoid macro scopes in error message 2020-12-11 11:23:44 -08:00
unknownId.lean.expected.out
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
unsound.lean fix: missing check at infer_proj 2022-02-25 07:15:34 -08:00
unsound.lean.expected.out
unused_univ.lean
unused_univ.lean.expected.out
unusedLet.lean fix: preserve unused let declarations 2021-10-18 17:40:15 -07:00
unusedLet.lean.expected.out
unusedWarningAtStructUpdate.lean
unusedWarningAtStructUpdate.lean.expected.out
updateExprIssue.lean
updateExprIssue.lean.expected.out chore: update expected test outputs 2025-06-20 17:29:10 +02: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
warningAsError.lean
warningAsError.lean.expected.out
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 chore: fix tests 2021-03-10 18:45:22 -08:00
whnfProj.lean.expected.out
wildcardAlt.lean
wildcardAlt.lean.expected.out feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
withAssignableSyntheticOpaqueBug.lean
withAssignableSyntheticOpaqueBug.lean.expected.out
withLocation.lean
withLocation.lean.expected.out
withLocationImplementationDetails.lean
withLocationImplementationDetails.lean.expected.out
withSetOptionIn.lean feat: guard_msgs to treat trace messages separate (#8267) 2025-05-09 05:44:34 +00:00
withSetOptionIn.lean.expected.out 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