max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab
History
Exact
Kyle Miller 47e96cd458
feat: add module features to #where command (#13811) 
This PR updates the `#where` command to be able to report
`module`-related scope state, for example a `@[expose] public meta
section` line in the output.
2026-05-21 18:11:43 +00:00
..
readDir.lean.dir
.gitattributes
.gitignore
28.lean
29.lean
34.lean
52_lean3.lean
91_lean3.lean
102_lean3.lean
108.lean
111.lean
121.lean
125.lean
175.lean
220.lean
220.lean.out.expected
223.lean
223.lean.out.expected
229.lean
229.lean.out.expected
236.lean
236.lean.out.expected
262.lean
269.lean
270.lean feat: beta reduce while elaborating applications (#13807) 2026-05-21 07:26:00 +00:00
280.lean
281.lean
282.lean
303.lean
305.lean
307.lean
307.lean.out.expected
310.lean
319.lean
326.lean
327.lean
329.lean
335.lean
337.lean
337.lean.out.expected
338.lean
338.lean.out.expected
341.lean
343.lean feat: have level metavariable pretty printer instantiate level metavariables (#13438) 2026-04-18 01:07:22 +00:00
345.lean
366.lean
366.lean.out.expected
382.lean
382.lean.out.expected
387.lean
394.lean
394.lean.out.expected
414.lean
414.lean.out.expected
415.lean
415.lean.out.expected
421.lean
421.lean.out.expected
435b.lean
436.lean
436_lean3.lean
439.lean
439.lean.out.expected
441.lean
445.lean
445.lean.out.expected
447_lean3.lean
447_lean3.lean.out.expected
452.lean
456.lean feat: have level metavariable pretty printer instantiate level metavariables (#13438) 2026-04-18 01:07:22 +00:00
457.lean
457.lean.out.expected
461a.lean
461b.lean
462.lean
463.lean
469.lean
469.lean.out.expected
470_lean3.lean
471.lean
474.lean
474.lean.out.expected feat: informative metavariable hovers, better delayed assignment pretty printing (#13446) 2026-04-23 01:43:55 +00:00
474_lean3.lean
474_lean3.lean.out.expected
481.lean
482.lean
490.lean
492.lean
492_lean3.lean
492_lean3.lean.out.expected
498.lean
498.lean.out.expected
500_lean3.lean
500_lean3.lean.out.expected
501.lean
501.lean.out.expected
509.lean
529.lean
529.lean.out.expected
536.lean
561.lean
569.lean
602.lean
602.lean.out.expected
604.lean
604.lean.out.expected
616.lean
620.lean
620.lean.out.expected
625.lean
625.lean.out.expected
633.lean
644.lean
646.lean
646.lean.out.ignored
654.lean
664.lean
677.lean
679.lean
679.lean.out.expected
696.lean
714.lean
714.lean.out.expected
716.lean
753.lean
760.lean
764.lean
764.lean.out.expected
783.lean
788.lean
790.lean
793.lean
796.lean
801.lean
801.lean.out.expected
813.lean
813.lean.out.expected
815.lean
815b.lean
815b.lean.out.expected
821.lean
837.lean
847.lean
854.lean
854.lean.out.expected
860.lean
879.lean
891.lean
909.lean
944.lean
945.lean
946.lean
948.lean
948.lean.out.expected
951.lean
951.lean.out.expected
955.lean
968.lean
972.lean
973.lean
973b.lean
973b.lean.out.expected
974.lean
983.lean
983.lean.out.expected
986.lean
988.lean
988.lean.out.expected
998.lean
998Export.lean
1016.lean
1017.lean
1017.lean.out.expected
1018.lean
1020.lean
1021.lean
1021.lean.out.expected
1022.lean
1024.lean
1024.lean.out.expected
1025.lean
1025.lean.out.expected
1026.lean
1026.lean.out.expected
1027.lean
1027.lean.out.expected
1029.lean
1030.lean
1037.lean
1039.lean
1039.lean.out.expected
1051.lean
1051.lean.out.expected
1058.lean
1074a.lean
1080.lean
1080.lean.out.expected
1098.lean
1098.lean.out.expected
1112.lean
1113.lean
1113.lean.out.expected
1113b.lean
1113b.lean.out.expected
1118.lean
1120.lean
1123.lean
1124.lean
1127.lean
1127.lean.out.expected
1132.lean
1143.lean
1155.lean
1156.lean
1158.lean
1163.lean
1163.lean.out.expected
1168.lean
1169.lean
1171.lean
1171.lean.out.expected
1179b.lean
1179b.lean.out.expected feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
1182.lean
1184.lean
1192.lean
1193a.lean
1193b.lean
1194.lean
1200.lean
1202.lean
1206.lean
1224.lean
1228.lean
1228.lean.out.expected
1230.lean
1230.lean.out.expected
1234.lean
1235.lean
1235.lean.out.expected
1236.lean
1237.lean
1237.lean.out.expected
1247.lean
1253.lean
1267.lean
1267.lean.out.expected
1274.lean
1275.lean
1275.lean.out.expected
1279.lean
1279.lean.out.expected
1279_simplified.lean
1279_simplified.lean.out.expected
1289.lean
1289.lean.out.expected
1292.lean
1292.lean.out.expected
1293.lean
1298.lean
1298.lean.out.expected
1299.lean
1300.lean
1302.lean
1305.lean
1308.lean
1308.lean.out.expected
1311.lean
1321.lean
1321.lean.out.expected
1333.lean
1337.lean
1342.lean
1342.lean.out.expected
1359.lean
1360.lean
1361.lean
1361.lean.out.expected
1361b.lean
1361b.lean.out.expected
1363.lean
1365.lean
1367.lean
1367.lean.out.expected
1372.lean
1373.lean
1374.lean
1375.lean
1375.lean.out.expected
1377.lean
1377.lean.out.expected
1380.lean
1380.lean.out.expected
1385.lean
1385.lean.out.expected
1389.lean
1408.lean
1408.lean.out.expected
1411.lean
1419.lean
1419.lean.out.expected
1420.lean
1426.lean
1426.lean.out.expected
1435.lean
1435.lean.out.expected
1436.lean
1441.lean
1547.lean
1549.lean
1558.lean
1571.lean
1571.lean.out.expected
1575.lean
1615.lean
1650.lean
1650.lean.out.expected
1668.lean
1668.lean.out.expected
1674.lean
1679.lean
1681.lean
1681.lean.out.expected
1684.lean
1684.lean.out.expected
1686.lean
1692.lean
1697.lean
1711.lean
1725.lean
1730.lean
1763.lean
1763.lean.out.expected
1779.lean
1779.lean.out.expected
1780.lean
1785.lean
1787.lean
1804.lean
1804.lean.out.expected
1808.lean
1812.lean
1812.lean.out.ignored
1813.lean
1813.lean.out.expected
1815.lean
1815.lean.out.expected
1822.lean
1829.lean feat: add warning when applying global attribute using in (#13223) 2026-04-08 06:20:34 +00:00
1834.lean
1841.lean
1842.lean
1842.lean.out.expected
1848.lean
1850.lean
1851.lean
1852.lean
1856.lean
1856.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
1869.lean
1870.lean
1878.lean
1878.lean.out.expected
1882.lean
1883.lean
1886.lean
1891.lean
1891.lean.out.expected
1892.lean
1892.lean.out.expected
1900.lean
1901.lean
1901.lean.out.expected
1907.lean
1907orig.lean
1910.lean
1918.lean
1921.lean
1926.lean
1926.lean.out.expected
1937.lean
1951.lean
1954.lean
1963.lean
1963.lean.out.expected
1968.lean
1985.lean
1986.lean
1986.lean.out.expected
2005.lean
2005.lean.out.expected
2009.lean
2018.lean
2018.lean.out.expected
2042.lean fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
2044.lean
2045.lean
2045.lean.out.expected
2058.lean fix: pp.universes should not affect constants with no universe levels (#13761) 2026-05-17 01:41:04 +00:00
2073.lean
2074.lean
2077.lean
2077.lean.out.expected
2079.lean
2079.lean.out.expected
2095.lean
2115.lean
2115.lean.out.expected
2136.lean
2136.lean.out.expected
2137.lean
2143.lean
2159.lean
2161.lean
2173.lean
2178.lean
2182.lean
2186.lean
2188.lean
2199.lean
2220.lean
2226.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
2243.lean
2249.lean
2262.lean
2265.lean
2265.lean.out.expected
2282.lean
2283.lean
2283.lean.out.expected
2291.lean
2291.lean.out.expected
2299.lean
2311.lean
2344.lean
2361.lean
2461.lean
2500.lean
2505.lean
2505.lean.out.expected
2514.lean
2552.lean
2558.lean
2558.lean.out.expected
2575.lean
2602.lean
2611.lean
2615.lean
2649.lean
2649.lean.out.expected
2669.lean
2669.lean.out.expected
2670.lean
2672.lean
2689.lean
2690.lean
2710.lean
2736.lean
2736.lean.out.expected
2810.lean
2835.lean
2843.lean
2843.lean.out.expected
2846.lean
2846.lean.out.expected
2862.lean
2899.lean
2899.lean.out.expected
2901.lean
2905.lean
2914.lean
2916.lean
2939.lean
2942.lean
2966.lean
3022.lean
3022.lean.out.expected
3031.lean
3045.lean
3057.lean
3057.lean.out.expected
3079.lean
3091.lean
3091.lean.out.expected
3140.lean
3140.lean.out.expected
3146.lean
3150.lean
3214.lean
3219.lean
3229.lean
3242.lean
3257.lean
3257.lean.out.expected
3313.lean
3386.lean
3395.lean
3458_1.lean
3458_2.lean
3467.lean
3497.lean
3501.lean
3519.lean
3524.lean
3524.lean.out.expected
3546.lean
3547.lean
3554.lean
3643.lean
3686.lean
3705.lean
3705.lean.out.expected
3706.lean
3710.lean
3713.lean
3731.lean
3740.lean
3745.lean
3791.lean
3807.lean
3807.lean.out.ignored
3922.lean
3943.lean
3943.lean.out.expected
3965.lean
3965.lean.out.expected
3965_2.lean
3965_2.lean.out.expected
3965_3.lean
3965_3.lean.out.expected
3996.lean
4051.lean
4051.lean.out.expected
4064.lean
4086.lean
4086.lean.out.expected
4089.lean
4089.lean.out.expected
4101.lean
4144.lean feat: beta reduce while elaborating applications (#13807) 2026-05-21 07:26:00 +00:00
4171.lean
4171.lean.out.expected
4203.lean
4213.lean
4219.lean
4230.lean
4240.lean
4240.lean.out.expected
4251.lean
4278.lean
4290.lean
4290.lean.out.expected
4306.lean
4310.lean
4313.lean
4318.lean
4320.lean
4334.lean
4339.lean
4365.lean
4375.lean
4381.lean
4390.lean
4390.lean.out.expected
4398.lean
4405.lean
4406.lean
4413.lean
4452.lean
4452.lean.out.expected
4462.lean
4462.lean.out.expected
4465.lean
4534.lean
4547.lean
4555.lean
4561.lean
4573.lean
4585.lean
4585.lean.out.expected
4591.lean
4591.lean.out.expected
4595_slowdown.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
4595_slowdown.lean.out.expected fix: add checkSystem calls to hasAssignableMVar (#13219) 2026-03-31 19:27:15 +00:00
4595_split.lean
4595_split.lean.out.expected
4636.lean
4636.lean.out.expected
4644.lean
4662.lean
4670.lean
4673.lean
4673.lean.out.expected
4677.lean
4686.lean
4716.lean
4751.lean
4761.lean
4761.lean.out.expected
4768.lean
4773.lean
4845.lean
4845.lean.out.expected
4851.lean
4861.lean
4861.lean.out.expected
4888.lean
4920.lean
4928.lean
4947.lean
4983.lean
4985.lean
5046.lean
5046.lean.out.expected
5064.lean
5126.lean
5176.lean
5236.lean
5333.lean
5333.lean.out.expected
5359.lean
5359.lean.out.expected
5388.lean
5406.lean
5407.lean
5417.lean
5424.lean
5455.lean
5455.lean.out.expected
5475.lean
5565.lean
5634.lean
5660.lean
5664.lean
5667.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
5668.lean
5672.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
5674.lean
5689.lean
5755.lean
5755.lean.out.expected
5818.lean
5993.lean
6043.lean
6065.lean
6065.lean.out.expected
6067.lean
6067.lean.out.expected
6086.lean
6090.lean
6117.lean
6123_cat_adjunction.lean
6123_cat_adjunction.lean.out.expected
6123_mod_cast.lean
6123_mod_cast.lean.out.expected
6164.lean
6199.lean
6263.lean
6263.lean.out.expected
6332.lean
6354.lean
6373.lean
6400.lean
6467.lean
6467.lean.out.expected
6601.lean
6655.lean
6694.lean
6706.lean
6759.lean
6789.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
6927.lean
6957.lean
6999.lean
7073.lean
7096.lean
7170.lean
7353.lean
7405.lean
7458.lean
7475.lean
7612.lean
7612.lean.out.expected
7638.lean
7788.lean
7811.lean
7927.lean
7993.lean
8049.lean
8067.lean
8721.lean
8743.lean feat: allow field notation to use explicit universe levels (#13262) 2026-04-09 13:29:10 +00:00
8815.lean
8894.lean
8938.lean
9089.lean
9156.lean
9312.lean
9322.lean
9322.lean.out.expected
9362.lean
9363.lean
9365.lean
9366.lean
9389.lean
9445.lean
9463.lean fix: deriving Inhabited for structures should inherit Inhabited instances (#13395) 2026-04-14 02:46:07 +00:00
9474.lean
9541.lean
9581.lean
9591.lean
9624.lean
9692.lean
9806.lean
9806.lean.out.expected
9893.lean feat: MVarId.assertAfter fvar alias info, MVarId.replace mvar dependencies, specialize tactic using eta arguments (#13528) 2026-04-30 10:36:29 +00:00
9937.lean
9963.lean
9971.lean
10067.lean
10078.lean
10078.lean.out.expected
10172.lean
10172.lean.out.expected
10181.lean
10196.lean
10213.lean
10234.lean
10234.lean.out.expected
10443.lean
10475.lean
10564.lean
10577.lean
10687.lean
10687.lean.out.expected
10753.lean feat: no default values for structure instance notation patterns (#13243) 2026-04-03 03:25:23 +00:00
10771.lean
10850.lean
10934.lean
10984.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
11115.lean
11322.lean
11337.lean
11389.lean
11509.lean
11687.lean
11719.lean
11747.lean
11773.lean
11778.lean
11823.lean
12025.lean
12048.lean
12136.lean
12138.lean
12172_regression.lean
12215.lean
12215.lean.out.expected
12229.lean test: regression tests for do issues fixed by the new elaborator (#13541) 2026-04-29 14:37:23 +00:00
12334.lean
12386.lean
12457.lean
12559.lean
12563.lean
12676.lean
12815.lean
12897.lean
13043.lean
13203.lean fix: make FirstTokens.seq (.optTokens _) .unknown return .unkown (#13205) 2026-04-01 13:21:26 +00:00
13268.lean fix: end_local_scope does not work with compound namespace names (#13360) 2026-04-13 10:05:26 +00:00
13268.lean.out.expected fix: end_local_scope does not work with compound namespace names (#13360) 2026-04-13 10:05:26 +00:00
13269.lean feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
13313.lean fix: make delta-derived instances respect enclosing meta sections (#13315) 2026-04-16 09:18:54 +00:00
13371.lean fix: include ignoreNoncomputable in LCNF cache key (#13384) 2026-04-13 09:27:25 +00:00
13407.lean fix: expand reset reuse in the presence of double oproj (#13421) 2026-04-15 19:16:22 +00:00
13415.lean fix: coinductive syntax causing panic in macro scopes (#13420) 2026-04-15 18:50:31 +00:00
13485.lean fix: preserve nesting level across empty doc snippet nesting (#13489) 2026-04-21 12:58:52 +00:00
13581.lean fix: withoutExporting around diagnostic reporting (#13630) 2026-05-06 13:47:26 +00:00
13768.lean fix: widen transparency field to 3 bits in Meta.Config cache key (#13768) 2026-05-18 10:51:59 +00:00
13770.lean fix: include zetaUnused in Meta.Config cache key (#13772) 2026-05-18 12:47:19 +00:00
abst.lean
abst.lean.out.expected
abstractExpr.lean
abstractMVars.lean
ac_expr.lean
ac_expr.lean.out.expected
ac_rfl.lean
ac_rfl.lean.out.expected
ack.lean
acLt_timeout.lean fix: prevent a hang in acLt (#13367) 2026-04-17 21:46:29 +00:00
ACltBug.lean
adam1.lean
adam1.lean.out.expected
adamTC.lean
adamTC2.lean
add_suggestion.lean
addDecorationsWithoutPartial.lean
addPPExplicitToExposeDiff.lean
aesop_run_metam.lean
aig_optimizations.lean
aig_stress.lean
alex1.lean
alex1.lean.out.expected
alg.lean
alias.lean
allFieldForConstants.lean
allFieldForConstants.lean.out.expected
allGoals.lean
and_intros.lean
andCasesOnBug.lean
anonymous_ctor_error_msg.lean
anonymousCtor.lean
appFinalizeIssue.lean
appFinalizeIssue.lean.out.expected
appIssue.lean
apply_error.lean
apply_subgoal_name_issue.lean fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
apply_tac.lean
applytransp.lean
appParserIssue.lean
appParserIssue.lean.out.expected
approxDepth.lean
approxDepth.lean.out.expected
array1.lean
array1.lean.out.expected
array_isEqvAux.lean
array_simp.lean
arrayDecEq.lean
arrayGetU.lean
arrayGetU.lean.out.expected
arrowDot.lean
arthur1.lean
arthur2.lean
arthur2.lean.out.expected
as_aux_lemma.lean
assertAfterBug.lean
assertAfterBug.lean.out.expected
assertExists.lean
aStructPerfIssue.lean
async.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async.lean.out.expected
async_base_functions.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_cancellation.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_cancellation_reasons.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_dns.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_body.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_body_framing.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_dispatch.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_encode.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_expect.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_fuzz.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_fuzz_limits.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_fuzz_random.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_h1_incremental.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_h1_parser_fuzz.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_h1_rfc_compliance.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_hang_regressions.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_headers.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_keepalive.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_request_headers.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_request_line.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_response_framing.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_string_quoting.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_trailers.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_http_uri.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_select_channel.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_select_gate.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_select_socket.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_select_socket.lean.out.expected
async_select_timer.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_sleep.lean
async_streammap.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_surface_sleep.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_systems_info.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_systems_info.lean.out.ignored
async_tcp_fname_errors.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_tcp_half.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_tcp_server_client.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
async_udp_sockets.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
atomValidation.lean
attachJp.lean
attachJp.lean.out.expected
attributeErrors.lean
autoboundIssues.lean
autoboundIssues.lean.out.expected
autoImplicitChain.lean
autoImplicitChain.lean.out.expected
autoLift.lean
autoLiftIssue.lean
autoparam.lean
autoparam.lean.out.expected
auxinvariable.lean
auxParentProj.lean
auxParentProj.lean.out.expected
backtrackable_estate.lean
balg.lean
baseIO.lean
baseIO.lean.out.expected
betaSimp.lean
bhaviksSampler.lean
bhaviksSampler.lean.out.expected
bigctor.lean
bigFromJson.lean
bigmul.lean
bigop.lean
bigop.lean.out.expected
bindCasesIssue.lean
bindCasesIssue.lean.out.ignored
binder_predicates.lean
binder_predicates.lean.out.expected
binderCacheIssue.lean
binderCacheIssue.lean.out.expected
binderCacheIssue2.lean
binderCacheIssue2.lean.out.expected
binderNameHint.lean
binderNameHint_congr.lean
binderNameHintScope.lean
binderNameHintSimp.lean
binderNotation.lean
binderNotation.lean.out.expected
bindersAbstractingUnassignedMVars.lean
bindersAbstractingUnassignedMVars.lean.out.expected
binop.lean
binop_binrel_perf_issue.lean
binop_binrel_perf_issue.lean.out.expected
binop_lazy.lean
binop_lazy.lean.out.expected
binopInfoTree.lean
binopInfoTree.lean.out.expected
binrec.lean
binrec.lean.out.ignored
binrel.lean
binrel_binop.lean
binrel_binop.lean.out.expected
binrelmacros.lean
binrelmacros.lean.out.expected
binsearch.lean
binsearch.lean.out.expected
bintreeGoal.lean
bintreeGoal.lean.out.expected
bitvec.lean
bitvec_fin_literal_norm.lean
bitvec_fin_literal_norm.lean.out.expected
bitvec_simproc.lean
bitwise.lean
bitwise.lean.out.expected
bool2int.lean
bool2int.lean.out.expected
bool_simp.lean
borrowBug.lean
boxing_bug.lean
broadcast.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
bubble.lean
bugNatLitDiscrTree.lean
builtinInitStx.lean
builtinSimprocTrace.lean
builtinSimprocTrace.lean.out.expected
bv_arith.lean
bv_axiom_check.lean
bv_bitblast_stress.lean
bv_bitwise.lean
bv_cast.lean
bv_counterexample.lean
bv_decide_bool.lean
bv_decide_enum_dependent.lean
bv_decide_enum_universe.lean
bv_decide_enums_two.lean
bv_decide_nat.lean
bv_decide_rewriter.lean
bv_decide_rewriter.lean.out.expected
bv_decide_rewriter_ac_nf.lean
bv_decide_shift_error.lean
bv_decide_shift_to_nat.lean
bv_decide_solver_modes.lean
bv_enums.lean
bv_errors.lean
bv_extract.lean
bv_inequality.lean
bv_llvm.lean
bv_math_lit_perf.lean
bv_math_lit_perf.lean.out.expected
bv_parametric_struct.lean
bv_popcount.lean
bv_preprocess_stress.lean
bv_reflection_stress.lean
bv_relation.lean
bv_shift.lean
bv_sint.lean
bv_structures.lean
bv_substructure.lean
bv_uint.lean
bv_uninterpreted.lean
bv_unused.lean
bv_will_overflow.lean
bvarcrash.lean
by_cases.lean
byAsSorry.lean
byCasesMetaM.lean
byCasesMetaM.lean.out.expected
bytearray.lean
bytearray.lean.out.expected
bytearray_eq.lean perf: use memcmp for ByteArray equality (#13235) 2026-04-01 15:30:03 +00:00
byteslice.lean
byteSliceIssue.lean
byteSliceIssue.lean.out.expected
cacheIssue.lean
cacheIssue.lean.out.expected
calc.lean
calc.lean.out.expected
calcBug.lean
calcInType.lean
cancel_token.lean refactor: keep IO.CancelToken task private, resolve promise before setting flag (#13569) 2026-04-29 11:12:54 +00:00
cancellation_context.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
canonM_exists_fun.lean
casePrime.lean
casesAnyTypeIssue.lean
casesOnAcc.lean
casesOnCases.lean
casesOnSameCtor.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
casesRec.lean
casesTactic.lean
casesUsing.lean
casesUsing.lean.out.expected
caseTacInMacros.lean
catchThe.lean
cbv1.lean
cbv2.lean
cbv3.lean
cbv4.lean
cbv_annotations2.lean
cbv_annotations3.lean
cbv_annotations4.lean
cbv_annotations5.lean
cbv_annotations6.lean
cbv_array.lean
cbv_at.lean
cbv_brackets.lean
cbv_classical.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
cbv_decidable_congr.lean
cbv_decide_simproc.lean
cbv_dep_proj.lean
cbv_eval_erase.lean
cbv_eval_inv.lean
cbv_hashmap_annotations.lean
cbv_ite_issue.lean
cbv_iter.lean
cbv_max_steps.lean
cbv_nullary.lean
cbv_opaque_guard.lean
cbv_opaque_inline.lean
cbv_opaque_reducible.lean chore: align cbv tactic with SymM framework conventions (#13682) 2026-05-11 10:04:26 +00:00
cbv_proj_arg_bug.lean
cbv_simproc.lean
cbv_simproc_errors.lean
cbv_simproc_fib.lean
cbv_string.lean
cbv_string_split.lean
cceScoping.lean
cdotAtSimpArg.lean
cdotTests.lean
cdotTuple.lean
cdotTuple.lean.out.expected
change.lean
charQuote.lean
charrange.lean
check.lean
check_failure.lean
check_failure.lean.out.expected
checkAssignmentIssue.lean
choiceExpectedTypeBug.lean
choiceExpectedTypeBug.lean.out.expected
choiceMacroRules.lean
choiceMacroRules.lean.out.expected
class_inductive.lean
class_inductive.lean.out.expected
classAbbrev.lean
classDefReducibilityAfterAttr.lean
classical.lean
cleanup_forallTelescope.lean
cleanupTypeAnnotations.lean
clear_value.lean
closure1.lean
codeBindUnreachIssue.lean
codeBindUnreachIssue.lean.out.ignored
coe.lean
coe.lean.out.expected
coeAttr1.lean
coeAttr1.lean.out.expected
coeAttrs.lean
coeIssue1.lean
coeIssue1.lean.out.expected
coeIssue2.lean
coeIssue2.lean.out.expected
coeIssue3.lean
coeIssue3.lean.out.expected
coeIssues4.lean
coelambda.lean
coeM.lean
coeM.lean.out.expected
CoeNew.lean
CoeNew.lean.out.expected
coeOutParamIssue.lean
coeOutParamIssue2.lean
coeOutParamIssue2.lean.out.expected
coeSort1.lean
coeSort2.lean
coeSort2.lean.out.expected
coinductive_instance.lean
coinductive_instance.lean.out.expected
coinductive_predicates.lean
coinductive_predicates_errors.lean
coinductive_syntax.lean perf: correct over-allocated capacity for imported constant hashmaps (#13238) 2026-04-03 08:58:42 +00:00
collectAxioms.lean
collectLooseBVars.lean
combinatorsAndWF.lean
CommandExtOverlap.lean
compatibleTypesEtaIssue.lean
compatibleTypesEtaIssue.lean.out.expected
compile_borrowed_reset_jp.lean
compile_coalesce_rc.lean
compile_drop_specialization.lean perf: dec specialization (#13788) 2026-05-19 19:56:34 +00:00
compile_multi_panic.lean
compile_recursive_array_access.lean
compiler_bug_neutral.lean
compiler_disable_borrow_annotations.lean
compiler_erase_bug.lean
compiler_proj_bug.lean
compiler_push_proj.lean perf: dec specialization (#13788) 2026-05-19 19:56:34 +00:00
compiler_type_transparency.lean
computedFields.lean
computedFieldsCode.lean
computedFieldsCode.lean.out.expected
concatElim.lean
config_eval.lean feat: efficient tactic configuration elaborators and configurability (#13651) 2026-05-14 17:20:57 +00:00
congrReserved.lean
congrSimpBug.lean
congrSimpDeclKinds.lean
congrSimpMathlibIssue.lean
congrTactic.lean
congrThm.lean
congrThm.lean.out.expected
congrThm2.lean
congrThm3.lean
congrThmIssue.lean
congrThmIssue.lean.out.expected
constant_fold_task_get_pure.lean
constantCompilerBug.lean
constantCompilerBug.lean.out.expected
constDelab.lean
constDelab.lean.out.expected
constFun.lean
constFun2.lean
constProp.lean
constProp.lean.out.expected
constructor_as_variable.lean feat: verification of String.dropWhile and String.takeWhile (#13155) 2026-04-03 14:02:21 +00:00
consumePPHint.lean
consumePPHint.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
context_async.lean fix: timing issues and race conditions in ContextAsync.race (#13718) 2026-05-13 01:25:01 +00:00
contra.lean
contradiction1.lean
contradictionExfalso.lean
contradictionLoop.lean
conv1.lean
conv2.lean
conv_arg.lean
convcalc.lean
convClear.lean
convInConv.lean
convInConv.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
convPatternAtLetIssue.lean
convPatternAtLetIssue.lean.out.expected
convPatternMatchIssue.lean
convPatternMatchIssue.lean.out.expected
convZetaLetExt.lean
convZetaLetExt.lean.out.expected
core.lean
crashDiv0.lean
crlfToLf.lean
csimp_type_error.lean
csimpAttrAppend.lean
csimpAttrAppend.lean.out.expected
csimpAttrFn.lean
csimpCore.lean
ctor_layout.lean
ctor_layout.lean.out.expected
ctorAutoParams.lean
ctorAutoParams.lean.out.expected
ctorElim.lean
ctorFieldVisibilityHints.lean
ctorIdx.lean
ctorIdxHInj.lean
ctorMixedRelevance.lean
currentDir.lean
currentDir.lean.out.ignored
customEliminators.lean
cutsat_lia_deprecation.lean
Daniel1.lean
dateTimeOrd.lean
dbgMacros.lean
dbgMacros.lean.init.sh
dbgMacros.lean.out.expected
deBruijn.lean
decAuxBug.lean
decClassical.lean
decEq.lean
decEqMutualInductives.lean
decEqMutualInductives.lean.out.expected
decEqNonInjIndex.lean
decidability_timeout.lean
Decidable-decide-erasure.lean
decide_cbv1.lean
decide_cbv_errors.lean
decidelet.lean
decideNative.lean
decideNative.lean.out.expected
decideNativePanic.lean
decideNativePanic.lean.init.sh
decideNativePanic.lean.out.expected
decideTactic.lean
decideTacticKernel.lean
decimals.lean
decimals.lean.out.expected
declareConfigElabBug.lean
declareConfigElabIssue.lean
decreasingTacticUpdatedEnvIssue.lean
deep1.lean
def1.lean
def2.lean
def3.lean
def4.lean
def5.lean
def6.lean
def6.lean.out.expected
def7.lean
def8.lean
def9.lean
def10.lean
def11.lean
def12.lean
def13.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
def14.lean
def15.lean
def16.lean
def17.lean
def18.lean
def19.lean
def20.lean
defaultEliminator.lean
defaultInstanceWithPrio.lean
defaultInstanceWithPrio.lean.out.expected
defaultInstBacktrackIssue.lean
defaultInstBacktrackIssue.lean.out.expected
defaultValueParamIssue.lean
DefEqAssignBug.lean
defeqAttrib.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
defeqAttribStrictOnly.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
defEqVsWhnfI.lean
delabApp.lean
delabConst.lean refactor: keep IO.CancelToken task private, resolve promise before setting flag (#13569) 2026-04-29 11:12:54 +00:00
delabDoLetFun.lean
delabDoLetFun.lean.out.expected
delabMatch.lean
delabName.lean
delabOverApp.lean
delabOverApp.lean.out.expected
delabProjectionApp.lean
delabStdRange.lean
delabStructInst.lean
delabUnexpand.lean
delabUnexpand.lean.out.expected
deltaRedIndPredBelow.lean
demangling.lean
depElim1.lean
depElim1.lean.out.expected feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
depFieldIssue.lean
depFieldIssue.lean.out.ignored
depHd.lean
deprecated_arg.lean feat: add deprecated_arg attribute (#13011) 2026-03-30 10:20:44 +00:00
deprecated_module.lean feat: add deprecated_module (#13002) 2026-04-01 14:40:43 +00:00
deprecated_syntax.lean feat: add deprecated_syntax (#13108) 2026-04-01 10:51:59 +00:00
deprecated_syntax.lean.out.expected feat: add deprecated_syntax (#13108) 2026-04-01 10:51:59 +00:00
deprecatedModule.lean feat: add deprecated_module (#13002) 2026-04-01 14:40:43 +00:00
deprecatedOptions.lean feat: allow deprecating options (#13195) 2026-04-02 14:44:11 +00:00
deq.lean
deriv.lean
deriving_diamond_defeq.lean fix: make delta-derived Prop-valued instances theorems (#13304) 2026-04-08 01:19:48 +00:00
derivingBEq.lean
derivingBEqLinear.lean refactor: use Nat.decEq in derived BEq instances (#13390) 2026-04-13 15:24:04 +00:00
derivingDecidableEq.lean
derivingDecidableEq.lean.out.expected
derivingDecidableEq2.lean
derivingDecidableEqLinear.lean
derivingDelta.lean fix: make delta-derived Prop-valued instances theorems (#13304) 2026-04-08 01:19:48 +00:00
derivingHashable.lean
derivingHashable.lean.out.expected
derivingHashable2.lean
derivingInhabited.lean
derivingNonempty.lean
derivingReflBEq.lean
derivingRepr.lean
derivingRpcEncoding.lean
derivingRpcEncoding.lean.out.expected
derivingToExpr.lean
diagnostics.lean
diagnosticsMsgOptional.lean
diagRec.lean
diamond1.lean
diamond2.lean
diamond2.lean.out.expected
diamond3.lean
diamond3.lean.out.expected
diamond4.lean
diamond4.lean.out.expected
diamond5.lean
diamond6.lean
diamond6.lean.out.expected
diamond7.lean
diamond7.lean.out.expected
diamond8.lean
diamond8.lean.out.expected
diamond9.lean
diamond9.lean.out.expected
diamond10.lean
diamond10.lean.out.expected
diamond11.lean
diamond12.lean
diamond13.lean
diff.lean
discrRefinement.lean
discrRefinement2.lean
discrRefinement3.lean
discrTreeIota.lean
discrTreeIota.lean.out.expected
discrTreeKey.lean
discrTreeKey.lean.out.expected
discrTreeOffset.lean
discrTreeSimp.lean
discrTreeSimp.lean.out.expected
divExact.lean
do_eqv.lean
do_eqv_proofs.lean
do_for_loop_compiler_test.lean feat: add warn.redundantExpose for redundant @[expose]/@[no_expose] attributes (#13359) 2026-04-27 10:33:58 +00:00
do_for_loop_levenstein_compiler_test.lean
doControlInfoAggregate.lean feat: inject unreachable! after break-less repeat (#13506) 2026-04-23 07:16:03 +00:00
docstringRewrites.lean
doDepIfAnon.lean fix: if _ : p ... syntax in new do elaborator (#13192) 2026-03-30 16:58:48 +00:00
doElemAsTermNotation.lean
doElemControlInfoAttribute.lean
doForInvariant.lean
doForMutSortPoly.lean fix: universe normalization in getDecLevel (#13391) 2026-04-14 21:27:22 +00:00
doForMutUniv.lean fix: use getDecLevel/isLevelDefEq for for loop mut var universe constraints (#13332) 2026-04-08 16:34:51 +00:00
dofun_prec.lean
doIfLet.lean
doIfLet.lean.out.expected
doLetArrowPatExpectedType.lean
doLetConfig.lean feat: add letConfig support to do block let/have (#13255) 2026-04-02 12:36:20 +00:00
doLetElse.lean
doLetElseIndent.lean
dollarProjIssue.lean
doLogicTests.lean
doMatchDependent.lean
doMatchDiscrDep.lean
doNotation1.lean
doNotation2.lean
doNotation3.lean
doNotation4.lean
doNotation5.lean
doNotation6.lean
doNotation6.lean.out.expected
doNotation7.lean test: regression tests for do issues fixed by the new elaborator (#13541) 2026-04-29 14:37:23 +00:00
doNotationIndexedMonad.lean feat: support more indexed monads in elabDoWith (#13801) 2026-05-20 17:59:25 +00:00
doNotationPluggableOps.lean feat: support more indexed monads in elabDoWith (#13801) 2026-05-20 17:59:25 +00:00
Dorais1.lean
Dorais1.lean.out.expected
doSyntaxPatternError.lean fix: surface meaningful pattern errors inside do-notation (#13542) 2026-04-27 21:12:04 +00:00
dotNameIssue.lean
dotNotationAndDefaultInstance.lean
dotNotationRecDecl.lean
doTrailingAtEOI.lean
dottedCtorNamedArgPattern.lean
dottedIdentNotation.lean
dottedNameBug.lean
double_match.lean
doubleReset.lean
doubleReset.lean.out.expected
dsimp1.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
dsimp2.lean
dsimp_bv_simproc.lean
dsimp_instances.lean
dsimp_proofs.lean
dsimpBackwardDefEqTrace.lean feat: add trace.Meta.Tactic.simp.backwardDefEq (#13640) 2026-05-05 13:02:27 +00:00
dsimpNatLitIssue.lean
dsimproc.lean
dsimpZetaIssue.lean
dsimpZetaIssue.lean.out.expected
due_to_metavariables.lean fix: free variable in do bind when continuation type depends on bvar (#13396) 2026-04-13 18:51:45 +00:00
duplicatedArgumentApplicationTypeMismatch.lean
dvd_simproc.lean
DVec.lean
DVec.lean.out.expected
dynamic.lean
eagerCoeExpansion.lean
eagerCoeExpansion.lean.out.expected
eagerInliningIssue.lean
elab_cmd.lean
elab_cmd.lean.out.expected
elabAsElim.lean
elabAsElim.lean.out.expected
elabCmd.lean
elabIte.lean
elabLet.lean
elabToSyntax.lean
elim_dead_vars.lean
elimDeadBranchesCtorParams.lean
elimDeadBranchesUInt64Literal.lean
elimDeadBranchesUInt64Literal.lean.out.expected
eliminatorImplicitTargets.lean
elimOptParam.lean
elseCaseArrow.lean
elseIfConfusion.lean
emptycOverloadIssues.lean
emptyEnvVar.lean
emptyLcnf.lean
endErrors.lean
enumDecEq.lean
enumNoConfusionIssue.lean
enumsModuloIrrelevance.lean
env_linter.lean refactor: turn dupNamespace into a Lean.Linter (#13708) 2026-05-12 06:39:08 +00:00
eq_some_iff_get_eq_issue.lean
eqndrecEtaLCNFIssue.lean
eqndrecEtaLCNFIssue.lean.out.expected
eqnOptions.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
eqnsAtSimp.lean
eqnsAtSimp.lean.out.expected
eqnsAtSimp2.lean
eqnsAtSimp3.lean
eqnsAtSimp3.lean.out.expected
eqnsPrio.lean
eqnsProjections.lean
eqnsReducible.lean
eqRecursors.lean
eqTheoremForVec.lean
eqThm.lean
eqThm.lean.out.expected
eqThmWithMoreThanOneAsPattern.lean
eqValue.lean
erased.lean
eraseReps.lean
eraseSimp.lean
eraseSimp.lean.out.expected
eraseSuffix.lean
erasureConfusion.lean
errorExplanationElab.lean
errorExplanationLinting.lean
eta.lean
eta.lean.out.expected
eta_lambda_lift.lean
etaFirst.lean
etaReducedMvarAssignments.lean
etaReducedMvarAssignments.lean.out.expected
etaStruct.lean
etaStruct.lean.out.expected
etaStructProofIrrelIssue.lean
eval.lean
eval_unboxed_const.lean
evalBuiltinInit.lean
evalCmd.lean
evalCmd.lean.out.expected
evalconst.lean
evalDo.lean
evalInit.lean
evalInit.lean.out.ignored
evalProp.lean
evalTacticBug.lean
exact_private.lean
exact_rw_deprecated.lean
exfalsoBug.lean
exists.lean
exp.lean
expandAbbrevAtIsClass.lean
expandExplicitBinders.lean
expandExplicitBinders.lean.out.expected
expandWhereStructInstIssue.lean
expectedTypePropagation.lean
explicitApp.lean
explicitApp.lean.out.expected
explicitMotive.lean
explicitOpenDeclIssue.lean
explicitOpenDeclIssue.lean.out.expected
exposeDiff.lean
exposeNames.lean
exposeNames.lean.out.expected
expr1.lean
expr_maps.lean
ExprLens.lean
ext.lean
ext1.lean
ext1.lean.out.expected
extensibleTacticBug.lean
extern.lean
externBoxing.lean
externBoxing.lean.out.expected
exthashset_deceq.lean
extmacro.lean
extract.lean
extract.lean.out.expected
extract_array_lit.lean
extract_lets.lean
extractClosed.lean
extraModUses.lean feat: efficient tactic configuration elaborators and configurability (#13651) 2026-05-14 17:20:57 +00:00
exttreeset_deceq.lean
exttreeset_deceq.lean.out.expected
false_or_by_contra.lean
falseElimAtSimpLocalDecl.lean
fib_correct.lean
fieldAbbrevInPat.lean
fieldAutoBound.lean
fieldDefaultValueWithoutType.lean
fieldIssue.lean
fieldNamesWithMinus.lean
fieldTypeBug.lean
fieldTypeBug.lean.out.ignored
filePath.lean
filePath.lean.out.expected
filter.lean
fin_coercions.lean
fin_two_pow.lean
finally.lean
finDotCtor.lean
finLit.lean
finMatch.lean
fixedIndexToParamIssue.lean
fixedIndexToParamIssue.lean.out.expected
fixedIndicesToParams.lean
fixedIndicesToParams.lean.out.expected
fixedParams.lean
fixedParamsAnnot.lean
fixedParamsDep.lean
fixedParamsReorder.lean
fixedParamsStructDeps.lean
flat_expr.lean
float1.lean
float32.lean
float_cases_bug.lean
float_conversions.lean
float_from_bignum.lean
floatarray.lean
floatBits.lean
floatLetIn.lean
floatOptParam.lean
foApprox.lean
fold_uint.lean
foldConsts.lean
foldLits.lean
foldLits.lean.out.expected
foldlUnsafe_bug.lean
foldProjs.lean
foldProjs.lean.out.expected
forallMetaBounded.lean
forallMetaBounded.lean.out.expected
forBodyResultTypeIssue.lean
forIn_phashset.lean
forInColErr.lean
forInElabBug.lean
forInListSpecUnivPoly.lean
forInListSpecUnivPoly.lean.out.expected feat: informative metavariable hovers, better delayed assignment pretty printing (#13446) 2026-04-23 01:43:55 +00:00
forInPArray.lean
forInRangeWF.lean
forInReturnPropagation.lean
forInUniv.lean
Format.lean
Format.lean.out.expected
formatHardLineBreaks.lean
formatTerm.lean
formatTerm.lean.out.expected
formatterTokenTable.lean
forOutParamIssue.lean
forOutParamIssue.lean.out.expected
forParallel.lean
french_ident.lean
french_quote.lean
frontend_meeting_2022_09_13.lean
frontend_meeting_2022_09_13.lean.out.expected feat: user-specified init fn when loading plugins (#13510) 2026-05-05 20:20:54 +00:00
fun.lean
fun.lean.out.expected
fun_cases.lean
funext.lean
funind_demo.lean
funind_expr.lean
funind_fewer_levels.lean
funind_mutual_dep.lean
funind_proof.lean
funind_structural.lean
funind_structural_mutual.lean
funind_tests.lean
funind_unfolding.lean
funInduction.lean
funinduction_generalize.lean
funinduction_ident.lean
funInfoBug.lean
funInfoBug.lean.out.expected
funMatchIssue.lean
fvarSubset.lean
gcd.lean
gcd.lean.out.expected
generalize.lean
generalizeMany.lean
generalizeTelescope.lean
genindices.lean
getArgPrime.lean
getElemV.lean chore: getElemV tests (#13249) 2026-04-02 21:24:04 +00:00
getline_crash.lean
getline_crash.lean.before.sh
globalAttributesIn.lean feat: add warning when applying global attribute using in (#13223) 2026-04-08 06:20:34 +00:00
grandparentImplicitReducible.lean
grind_9216.lean
grind_9321.lean
grind_9427.lean
grind_9467.lean
grind_9477.lean
grind_9485.lean
grind_9485.lean.out.expected
grind_9562.lean
grind_9572.lean
grind_9610.lean
grind_9769.lean
grind_9825.lean
grind_9828.lean
grind_9830.lean
grind_9854.lean
grind_9856.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
grind_9856.lean.out.expected
grind_9897.lean
grind_9899.lean
grind_9907.lean
grind_9948.lean
grind_10160.lean
grind_10160.lean.out.expected
grind_10232.lean
grind_10232.lean.out.expected
grind_10233.lean
grind_10233.lean.out.expected
grind_10317.lean
grind_10489.lean
grind_10500.lean
grind_10622.lean
grind_10622.lean.out.expected
grind_10661.lean
grind_10670.lean
grind_10885.lean
grind_10953.lean
grind_10983.lean
grind_11001.lean
grind_11001.lean.out.expected
grind_11036.lean
grind_11081.lean
grind_11081.lean.out.expected
grind_11086.lean
grind_11086.lean.out.expected
grind_11088.lean
grind_11124.lean fix: extend sym canonicalizer reductions to value positions (#13272) 2026-04-04 01:52:24 +00:00
grind_11124.lean.out.expected
grind_11130.lean
grind_11130.lean.out.expected
grind_11134.lean
grind_11134.lean.out.expected
grind_11259.lean
grind_11449.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
grind_11477.lean
grind_11498.lean
grind_11498.lean.out.expected
grind_11515.lean
grind_11539.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
grind_11539_2.lean
grind_11545.lean
grind_11545.lean.out.expected
grind_11597.lean
grind_11597.lean.out.expected
grind_11622.lean
grind_11633.lean
grind_11690.lean
grind_11690.lean.out.expected
grind_11697_a.lean
grind_11697_b.lean
grind_11738.lean
grind_11745.lean
grind_11745_extra.lean
grind_11930.lean
grind_12140.lean
grind_12246.lean
grind_12246.lean.out.expected
grind_12390.lean
grind_12428.lean
grind_12428.lean.out.expected
grind_12581.lean
grind_12812.lean
grind_13167.lean fix: expose grind gadgets abstractFn and simpMatchDiscrsOnly (#13177) 2026-03-29 10:37:54 +00:00
grind_13573.lean fix: disable model-based theory combination in grind derived tactics (#13593) 2026-05-01 01:45:17 +00:00
grind_abstract_mvars.lean
grind_ac_1.lean
grind_ac_2.lean
grind_ac_3.lean
grind_ac_4.lean
grind_ac_5.lean
grind_ac_inv_issue.lean fix: grind AC invariant (#13614) 2026-05-03 02:19:51 +00:00
grind_ac_inv_issue_2.lean fix: another grind AC invariant (#13622) 2026-05-03 13:33:13 +00:00
grind_activate_local_issue.lean
grind_all_singleton_patterns.lean
grind_alphaShare_builder.lean
grind_annotated.lean
grind_append_issue.lean
grind_append_issue.lean.out.expected
grind_arbitrary_params.lean
grind_arith_nonstd_insts.lean
grind_array.lean
grind_array_attach.lean
grind_assoc.lean
grind_assoc.lean.out.expected
grind_attrs.lean
grind_attrs.lean.out.expected
grind_beta.lean
grind_beta_generation_check.lean fix: beta reduction in grind must respect generation threshold (#13560) 2026-04-28 21:51:14 +00:00
grind_big_poly.lean
grind_bigstep.lean
grind_bintree.lean
grind_bintree.lean.out.expected
grind_bitvec.lean
grind_bool_diseq.lean
grind_bool_prop.lean
grind_canon_bug.lean
grind_canon_bug.lean.out.expected
grind_canon_bug_2.lean
grind_canon_insts.lean
grind_canon_insts.lean.out.expected
grind_canon_ofnat.lean
grind_canon_ofnat.lean.out.expected
grind_canon_types.lean
grind_canon_types.lean.out.expected
grind_cases.lean
grind_cases_tac.lean
grind_cases_tac.lean.out.expected
grind_casting_issue.lean
grind_cat.lean
grind_cat2.lean
grind_cat2.lean.out.expected
grind_clean_den.lean
grind_clear_error.lean
grind_clear_error.lean.out.expected
grind_commsemiring.lean
grind_congr.lean
grind_congr.lean.out.expected
grind_congr1.lean
grind_congr1.lean.out.expected
grind_congr_hash_issue.lean
grind_congr_over_applied.lean
grind_const_pattern.lean
grind_const_pattern.lean.out.expected
grind_constProp.lean
grind_constProp.lean.out.expected
grind_countP.lean
grind_ctor_ematch.lean
grind_ctor_ematch.lean.out.expected
grind_ctorIdx.lean
grind_cutsat_auto.lean
grind_cutsat_auto.lean.out.expected
grind_cutsat_commring.lean
grind_cutsat_cooper.lean
grind_cutsat_cooper.lean.out.expected
grind_cutsat_decompose.lean
grind_cutsat_diseq_1.lean
grind_cutsat_diseq_1.lean.out.expected
grind_cutsat_diseq_2.lean
grind_cutsat_diseq_2.lean.out.expected
grind_cutsat_diseq_3.lean
grind_cutsat_diseq_3.lean.out.expected
grind_cutsat_diseq_cooper.lean
grind_cutsat_diseq_cooper.lean.out.expected
grind_cutsat_div_1.lean
grind_cutsat_div_1.lean.out.expected
grind_cutsat_div_mod.lean
grind_cutsat_div_mod.lean.out.expected
grind_cutsat_eq_1.lean
grind_cutsat_eq_1.lean.out.expected
grind_cutsat_instances.lean
grind_cutsat_le_1.lean
grind_cutsat_le_1.lean.out.expected
grind_cutsat_le_2.lean
grind_cutsat_le_2.lean.out.expected
grind_cutsat_nat_dvd.lean
grind_cutsat_nat_dvd.lean.out.expected
grind_cutsat_nat_eq.lean
grind_cutsat_nat_eq.lean.out.expected
grind_cutsat_nat_le.lean
grind_cutsat_nat_le.lean.out.expected
grind_cutsat_natCast_propagation.lean
grind_cutsat_omega.lean
grind_cutsat_pow.lean
grind_cutsat_proof_term_issue.lean
grind_cutsat_tests.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
grind_cutsat_tests.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
grind_cutsat_toint_1.lean
grind_cutsat_trim_context.lean
grind_cutsat_upper_bug.lean
grind_cutsat_upper_bug.lean.out.expected
grind_cutsat_zero.lean
grind_decide_bool_issues.lean
grind_decide_bool_issues.lean.out.expected
grind_def_eq_inv_issue.lean fix: missing proof hints in grind propagators (#13623) 2026-05-03 14:51:03 +00:00
grind_dep_match_overlap.lean
grind_diseq.lean
grind_diseq_cancel_var_bug.lean
grind_dvd_propagate_issue.lean
grind_dvd_propagate_issue.lean.out.expected
grind_ematch1.lean
grind_ematch1.lean.out.expected
grind_ematch2.lean
grind_ematch2.lean.out.expected
grind_ematch_diag.lean feat: add E-matching diagnostics to grind (#13558) 2026-04-29 12:17:55 +00:00
grind_ematch_gen_pattern.lean
grind_ematch_gen_pattern.lean.out.expected
grind_ematch_ground_implicit_inst.lean
grind_ematch_patterns.lean
grind_ematch_patterns.lean.out.expected
grind_ematch_theorem_activation.lean
grind_ematch_theorem_activation.lean.out.expected
grind_ematch_type_error.lean
grind_eq.lean
grind_eq.lean.out.expected
grind_eq_bwd.lean
grind_eq_bwd.lean.out.expected
grind_eq_bwd_pat_bug.lean
grind_eq_bwd_pat_bug.lean.out.expected
grind_eq_false_of_imp_eq_false.lean
grind_eq_false_of_imp_eq_false.lean.out.expected
grind_eq_pattern.lean
grind_eqc_inv_issue.lean fix: grind congruence-table invariant for lazy ite branches (#13624) 2026-05-03 17:27:54 +00:00
grind_eqres_bug.lean
grind_erase_attr.lean
grind_erase_attr.lean.out.expected
grind_eta.lean
grind_eta_struct_internalize.lean
grind_eta_struct_internalize.lean.out.expected
grind_etaStruct.lean
grind_eval_suggest.lean
grind_eval_suggest.lean.out.expected
grind_exfalso.lean
grind_ExtTreeSet.lean
grind_fastEraseDups.lean
grind_field_div.lean
grind_field_norm.lean
grind_field_norm_2.lean
grind_field_panic.lean
grind_field_panic.lean.out.expected
grind_fin.lean
grind_fin_bug.lean
grind_fin_zero.lean
grind_finish_trace.lean
grind_finish_trace.lean.out.expected
grind_finVal.lean
grind_fun_singleton.lean
grind_funCC.lean
grind_funext.lean
grind_getElem.lean
grind_getElem.lean.out.expected
grind_getLast_dropLast.lean
grind_ground_pat_issue.lean
grind_ground_pat_issue.lean.out.expected
grind_ground_thm.lean
grind_guide.lean
grind_guide.lean.out.ignored
grind_guide_2.lean
grind_guide_2.lean.out.expected
grind_hashmap_list.lean
grind_hashmap_list.lean.out.expected
grind_hcongr.lean
grind_heapsort.lean
grind_heapsort.lean.out.expected
grind_heartbeats.lean
grind_heartbeats.lean.out.expected
grind_heq_proof_issue.lean
grind_human_eval_114.lean
grind_hyper_ex.lean
grind_ignore_impl_detail.lean
grind_implies.lean
grind_indexmap.lean
grind_indexmap_pre.lean
grind_indexmap_pre.lean.out.expected
grind_indexmap_trace.lean fix: handle propositional and decidable instances in sym canonicalizer (#13271) 2026-04-04 00:40:39 +00:00
grind_indexmap_trace.lean.out.expected
grind_inj.lean
grind_inj2.lean
grind_inj2.lean.out.expected
grind_inj_clear_issue.lean
grind_inst_mvars_issue.lean
grind_inst_mvars_issue.lean.out.expected
grind_intcast_natcast.lean
grind_interactive.lean
grind_interactive.lean.out.expected
grind_interactive_2.lean
grind_interactive_2.lean.out.expected
grind_internalize_bitvec_lit.lean
grind_internalize_bitvec_lit.lean.out.expected
grind_intmodule_eq_prop.lean
grind_issue_9125.lean
grind_issue_9187.lean
grind_ite.lean
grind_ite_congr.lean
grind_ite_parent.lean
grind_ite_split_issue.lean
grind_ite_trace.lean
grind_ite_trace.lean.out.expected
grind_ite_unused_match.lean
grind_ite_unused_match.lean.out.expected
grind_lawful_eq_cmp.lean
grind_lax.lean
grind_lax.lean.out.expected
grind_lazy_ite.lean
grind_lazy_ite.lean.out.expected
grind_lex.lean
grind_lia_regression.lean fix: case-split on arithmetic implications with And/Or antecedents (#13590) 2026-04-30 23:15:34 +00:00
grind_linarith_1.lean
grind_linarith_1.lean.out.expected
grind_linarith_2.lean
grind_linarith_2.lean.out.expected
grind_linarith_rational.lean
grind_linarith_spurious_issues.lean
grind_linarith_trim_context.lean
grind_linearize.lean
grind_lint_1.lean
grind_lint_array.lean
grind_lint_bitvec.lean
grind_lint_list.lean
grind_lint_misc.lean
grind_lint_std_hashmap.lean
grind_lint_std_misc.lean
grind_lint_std_treemap.lean
grind_list.lean
grind_list.lean.out.expected
grind_list3.lean
grind_list_count.lean
grind_list_drop_take.lean
grind_list_erase.lean
grind_list_find.lean
grind_list_issue.lean
grind_list_issue.lean.out.expected
grind_list_perm.lean
grind_list_sublist.lean
grind_local_hyps.lean
grind_locals.lean
grind_locals_module.lean
grind_lookahead.lean
grind_lookahead.lean.out.expected
grind_many_eqs.lean
grind_map.lean
grind_mark_nested_proofs_bug.lean
grind_match1.lean
grind_match1.lean.out.expected
grind_match2.lean
grind_match2.lean.out.expected
grind_match_cond_contra.lean
grind_match_cond_issue.lean
grind_match_cond_split.lean
grind_match_eq_propagation.lean
grind_match_with_eq.lean
grind_mbtc_1.lean
grind_mbtc_1.lean.out.expected
grind_mbtc_bad_splits.lean
grind_min.lean
grind_module_eqs.lean
grind_module_normalization.lean
grind_module_relations.lean
grind_mon_order.lean feat: add Sym.Arith infrastructure for arithmetic normalization (#13289) 2026-04-06 05:21:09 +00:00
grind_mon_order.lean.out.expected
grind_mvar.lean
grind_mvar.lean.out.expected
grind_mvar_hyps.lean
grind_nat_bitwise.lean
grind_nat_module.lean
grind_nat_module_2.lean
grind_nat_module_norm.lean
grind_nat_semiring.lean
grind_nat_sub_encoding.lean
grind_natCast.lean
grind_natCast_intCast.lean
grind_natCast_issue.lean
grind_natCast_nonneg_ring.lean
grind_nested_mdata.lean
grind_nested_proof_issue.lean
grind_nested_proofs.lean
grind_nested_proofs.lean.out.expected
grind_nochrono.lean
grind_noncomm_ring.lean
grind_noncomm_semiring.lean
grind_nonforall_params.lean
grind_nonlinear_occ_issue.lean
grind_norm.lean
grind_norm_levels.lean
grind_not_internalized.lean fix: grind cast internalization order (#13625) 2026-05-03 16:32:10 +00:00
grind_offset.lean
grind_offset.lean.out.expected
grind_omega_examples.lean
grind_omega_tests.lean
grind_one_mul.lean
grind_one_mul.lean.out.expected
grind_option.lean
grind_ord_module.lean
grind_order_1.lean
grind_order_2.lean
grind_order_3.lean
grind_order_eq.lean fix: kernel error in grind order module for Nat casts to non-Int types (#13453) 2026-04-17 23:51:21 +00:00
grind_order_issue.lean
grind_order_propagation.lean
grind_over_applied_nestedProof.lean
grind_overapplied_ite.lean
grind_overapplied_ite.lean.out.expected
grind_palindrome2.lean
grind_palindromes.lean
grind_palindromes.lean.out.expected
grind_panic_invariant.lean
grind_panic_invariant.lean.out.expected
grind_params.lean
grind_params.lean.out.expected
grind_pat_sel.lean
grind_pattern1.lean
grind_pattern2.lean
grind_pattern2.lean.out.expected
grind_pattern3.lean
grind_pattern_cnstr.lean
grind_pattern_cnstr.lean.out.expected
grind_pattern_cnstr_2.lean
grind_pattern_inference_issue.lean
grind_pattern_proj.lean
grind_pattern_scoped.lean
grind_pattern_validation_instance.lean
grind_Poly_mul_0_bug.lean
grind_pow_add_semiring.lean
grind_pow_identity.lean feat: wire PowIdentity into grind ring solver (#13088) 2026-04-08 10:14:10 +00:00
grind_pow_inst_issue.lean
grind_pow_inst_issue.lean.out.expected
grind_pow_zero.lean
grind_pp_attr.lean
grind_pre.lean
grind_pre.lean.out.expected
grind_preinstance_set_bug.lean
grind_preinstance_set_bug.lean.out.expected
grind_preord_module.lean
grind_primes.lean
grind_prod.lean
grind_product_eta_and_split.lean
grind_proof_perf_issue.lean
grind_prop_arrow.lean
grind_prop_arrow.lean.out.expected
grind_prop_inst.lean fix: handle propositional and decidable instances in sym canonicalizer (#13271) 2026-04-04 00:40:39 +00:00
grind_proveEqIssue.lean
grind_proveEqIssue.lean.out.expected
grind_qsort.lean
grind_qsort.lean.out.expected
grind_question_mark_suggestions.lean
grind_rat.lean
grind_reducible.lean
grind_reducible.lean.out.expected
grind_refl_cmp.lean
grind_regression.lean
grind_regression.lean.out.expected
grind_ring_1.lean feat: wire PowIdentity into grind ring solver (#13088) 2026-04-08 10:14:10 +00:00
grind_ring_1.lean.out.expected feat: wire PowIdentity into grind ring solver (#13088) 2026-04-08 10:14:10 +00:00
grind_ring_2.lean
grind_ring_2.lean.out.expected
grind_ring_3.lean
grind_ring_4.lean
grind_ring_degree_explosion.lean fix: limit ring solver polynomial degree in grind (#13585) 2026-04-30 14:00:00 +00:00
grind_ring_norm_ring_proof.lean
grind_ring_op_sanity_checks.lean
grind_ring_trim_context.lean
grind_section_var.lean
grind_semiring.lean
grind_semiring_norm.lean
grind_semiring_norm_regression.lean
grind_semiring_norm_regression.lean.out.expected
grind_set_config.lean
grind_set_config.lean.out.expected
grind_shelf.lean
grind_smul_issue.lean
grind_som1.lean
grind_sort_eqc.lean
grind_sort_eqc.lean.out.expected
grind_sort_intern.lean
grind_split.lean
grind_split.lean.out.expected
grind_split_arith_imp.lean
grind_split_arith_imp.lean.out.expected
grind_split_data.lean
grind_split_issue.lean
grind_split_issue.lean.out.expected
grind_spoly.lean fix: limit ring solver polynomial degree in grind (#13585) 2026-04-30 14:00:00 +00:00
grind_suggestions.lean
grind_sym_prio.lean
grind_sym_prio.lean.out.expected
grind_t1.lean
grind_t1.lean.out.expected
grind_toint_instances.lean
grind_toint_instances.lean.out.expected
grind_toInt_issue.lean
grind_toInt_mbtc.lean
grind_trace.lean
grind_trace.lean.out.expected
grind_trace_local_dot_notation.lean
grind_trace_term_params.lean
grind_trig.lean
grind_trig.lean.out.expected
grind_try_exact.lean
grind_try_exact.lean.out.expected
grind_try_extend.lean
grind_try_trace.lean
grind_try_trace.lean.out.expected
grind_unfold_reducible_issue.lean
grind_unfold_reducible_regression.lean
grind_unfold_reducible_regression.lean.out.expected
grind_univ_poly_ground_pattern.lean
grind_universe_polymorphism.lean
grind_unnecessary_hypothesis.lean feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
grind_unused_lemmas.lean
grind_usr.lean
grind_usr.lean.out.expected
grind_vector.lean
grind_warn_param.lean
grindDeprecated.lean
gring_11543.lean
gring_11543.lean.out.expected
guard_expr.lean
guard_msgs.lean feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
guard_msgs.lean.init.sh
guardexpr.lean
guessLex.lean
guessLex.lean.out.expected
guessLexTricky.lean
guessLexTricky.lean.out.expected
guessLexTricky2.lean
guessLexTricky2.lean.out.expected
handleLocking.lean
handleLocking.lean.before.sh
hashableBug.lean
hashmap-implicits.lean
hashmap-toList-simps.lean
hashmap.lean
hasNotBit.lean
haveDestruct.lean
haveI.lean
haveI.lean.out.expected
haveTactic.lean
hcongr.lean
hcongr.lean.out.expected
heapSort.lean
heapSort.lean.out.expected
heqSubst.lean
hexnum.lean
hinj_thm.lean
hintPreviewSpan.lean
hintSuggestionMessage.lean
hintWordDiff.lean
hlistOverload.lean
hmul2.lean
hmul2.lean.out.expected
hmulDefaultInstance.lean
hmulDefaultInstance.lean.out.expected
hpow.lean
hpow.lean.out.expected
idbg_basic.lean
idbg_e2e.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
idbg_e2e.lean.out.expected
idSuggestEvery.lean
idSuggestPostHoc.lean
idSuggestShort.lean
idSuggestStandalone.lean
ifcongr.lean
ifcongr.lean.out.expected
iffRefl.lean
ifThenElseIssue.lean
ifThenElseIssue2.lean
impByNameResolution.lean
impLambdaTac.lean
implDetailBinder.lean
implicit_reducible_list_length.lean
implicit_reducible_list_length.lean.out.expected
implicitApplyIssue.lean
implicitLambdaLocalWithoutType.lean
implicitRflProofs.lean
implicitTypesRecCoe.lean
importStructure.lean
impossibleInstance.lean feat: better error messages and more complete logic for checkImpossibleInstance and checkNonClassInstance (#13550) 2026-05-14 09:40:03 +00:00
inaccessibleAnnotDefEqIssue.lean
inaccessibleAnnotDefEqIssue.lean.out.expected
incmd.lean
incmd.lean.out.expected
ind_cmd_bug.lean
ind_whnf.lean
ind_whnf2.lean
index_variables_linter.lean fix: do not modify infotrees in withSetOptionIn (#11313) 2026-05-11 11:36:39 +00:00
indPredRecursion.lean
induction1.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
inductionAltExplicit.lean
inductionCheckAltNames.lean fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
inductionComplexMotive.lean
inductionLetIssue.lean
inductionParse.lean
inductionTacticBug.lean
inductive1.lean
inductive1.lean.out.expected
inductive2.lean
inductive2.lean.out.expected
inductive_mutual.lean
inductive_pred.lean
inductive_pred.lean.out.expected
inductive_rec_proj.lean
inductive_typestar.lean
inductive_univ.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
inductiveBinderUpdates.lean
inductiveIndicesIssue.lean
inductiveParamMismatchError.lean
indUsingLet.lean
indUsingTerm.lean
inferForallTypeLCNF.lean
inferForallTypeLCNF.lean.out.expected
inferInstanceAs.lean feat: detect further sub-instances in wrapInstance (#13536) 2026-05-02 11:55:04 +00:00
inferTypeFailure.lean
infixprio.lean
info_trees.lean feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
infoFromFailure.lean
initializeNonemptyErrorMsg.lean
initModule.lean fix: respect module visibility in initialize/builtin_initialize 2026-04-10 15:08:43 +02:00
inj1.lean
inj2.lean
injectionBug.lean
injections1.lean
injectionsIssue.lean
injective.lean
injHEq.lean
injIssue.lean
injSimp.lean
inline_fn.lean
inlineApp.lean
inlineExpr.lean
inlineIfReduceLCNF.lean
inlineIfReduceLCNF.lean.out.ignored
inlineIssue.lean
inlineLCNFIssue.lean
inlineLCNFIssue.lean.out.ignored
inlineLoop.lean
inlineProjInstIssue.lean
inliner_loop.lean
inlineWithNestedRecIssue.lean
inlineWithNestedRecIssue.lean.out.ignored
inst.lean
inst.lean.out.expected
instanceIssues.lean
instanceReducibility.lean
instanceReducible.lean
instances.lean
instances.lean.out.ignored
instanceUsingFalse.lean
instanceWhere.lean
instanceWhereDecls.lean
instantiateMVarsCrossScope.lean
instantiateMVarsShadow.lean
instantiateMVarsSharing.lean
instantiateRevBetaS.lean
instEtaIssue.lean
instPatVar.lean
instprio.lean
instuniv.lean
instuniv.lean.out.expected
int_complement_shiftRight.lean
int_div_mod.lean
int_to_nat_bug.lean
int_toBitVec.lean
internalizeCasesIssue.lean
interp.lean
interp.lean.out.expected
interp2.lean
interp2.lean.out.expected
intModBug.lean
intModBug.lean.out.expected
intNegSucc.lean
intNegSucc.lean.out.expected
intro.lean
introLetBug.lean
introLetBug.lean.out.expected
introLetFun.lean
intromacro.lean
invalid_dotted_identifier_prop.lean
invalid_field_notation_function.lean
invalid_field_notation_function.lean.out.expected
invalid_field_notation_mvar.lean
invalid_field_notation_unusable_param.lean
invalidProjection.lean
invalidTupleProjHints.lean
IO_test.lean
IO_test.lean.before.sh
ioNulBytes.lean
ioRandomBytes.lean
ioRandomBytes.lean.out.ignored
IRbug.lean
IRbug.lean.out.expected
irCompilerBug.lean
irreducibleIssue.lean
isDefEqCheckAssignmentBug.lean
isDefEqCheckAssignmentBug.lean.out.expected
isDefEqConstApproxIssue.lean
isDefEqIssue.lean
isDefEqMVarSelfIssue.lean
isDefEqMVarSelfIssue.lean.out.expected
isDefEqPerfIssue.lean
isDefEqPerfIssue.lean.out.expected
isDefEqProjIssue.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
isDefEqProjPerfIssue.lean
isDefEqProjPerfIssue.lean.out.expected
isInstanceCongrRegression.lean
isNoncomputable.lean
isNoncomputable.lean.out.expected
issue2102.lean
issue2108.lean
issue2113.lean
issue2171.lean
issue2237.lean
issue2628.lean
issue2628.lean.out.expected
issue2883.lean
issue2925.lean
issue2962.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
issue2975.lean
issue2975.lean.out.expected
issue2981.lean
issue2981.lean.out.expected
issue2982.lean
issue3175.lean
issue3204.lean
issue3212.lean
issue3212.lean.out.expected
issue3770.lean
issue3848.lean
issue4063.lean
issue4146.lean
issue4394.lean
issue4540.lean
issue4650.lean
issue4671.lean
issue4684.lean
issue4726.lean
issue5027.lean
issue5061.lean
issue5347.lean
issue5384.lean
issue5562.lean
issue5602.lean
issue5630.lean
issue5630.lean.out.expected
issue5661.lean feat: no [defeq] attribute on sizeOf_spec lemmas (#13320) 2026-04-08 11:10:50 +00:00
issue5699.lean
issue5726.lean
issue5767.lean
issue5767.lean.out.expected
issue5828.lean
issue5836.lean
issue5903.lean
issue6015.lean
issue6281.lean
issue6281.lean.out.expected
issue6531.lean
issue6550.lean
issue6592.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
issue6786.lean
issue7318.lean
issue7322.lean
issue7332.lean
issue7383.lean
issue7383.lean.out.expected
issue7408.lean
issue7550.lean
issue7826.lean
issue7826.lean.out.expected
issue7826a.lean
issue8093.lean
issue8098.lean
issue8103.lean
issue8107.lean
issue8195.lean
issue8213.lean
issue8257.lean
issue8274.lean
issue8293.lean
issue8360.lean
issue8490.lean
issue8939.lean
issue8939wf.lean
issue8939wf.lean.out.expected
issue8962.lean
issue8969.lean
issue9018.lean
issue9462.lean
issue9646.lean
issue9844.lean
issue9846.lean
issue10132.lean
issue10195.lean
issue10299.lean
issue10329.lean
issue10353.lean
issue10416.lean
issue10424.lean
issue10431.lean
issue10573.lean
issue10651.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
issue10678.lean
issue10683.lean
issue10705.lean
issue10710.lean
issue10721.lean
issue10723.lean
issue10749.lean feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
issue10775.lean
issue10781.lean
issue10792.lean
issue10794.lean
issue10821.lean
issue10895.lean
issue10976.lean
issue11181.lean
issue11183.lean
issue11186.lean
issue11211.lean feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
issue11221.lean
issue11342.lean
issue11449.lean
issue11450.lean
issue11560.lean
issue11610.lean
issue11655.lean
issue11665.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
issue11695.lean
issue12240.lean
issue12268.lean
issue12398.lean
issue12404.lean
issue12495.lean
issue12495.lean.out.expected
issue12543.lean
issue12630.lean
issue12630.lean.out.expected
issue12768.lean fix: free variable in do bind when continuation type depends on bvar (#13396) 2026-04-13 18:51:45 +00:00
issue12804.lean
issue12819.lean
issue12826.lean fix: improve error for join point assignment failure in do elaborator (#13397) 2026-04-13 19:32:43 +00:00
issue12846.lean fix: improve result type mismatch errors and locations in new do elaborator (#13404) 2026-04-16 09:16:27 +00:00
issue13015.lean fix: handle multi-discriminant casesOn in WF unfold equation generation (#13232) 2026-04-01 15:23:13 +00:00
issue13373.lean fix: generate SizeOf spec theorems for inductives with private constructors (#13374) 2026-04-12 12:00:51 +00:00
issue13444.lean fix: distinguish recursive applications by source position (#13645) 2026-05-05 16:40:29 +00:00
issue13691.lean fix: strip hypothesis-naming metadata from proof-mode targets (#13812) 2026-05-21 16:18:17 +00:00
issue13729.lean fix: respect fixed-parameter permutation when reporting structural recursion failures (#13730) 2026-05-14 08:17:13 +00:00
ite_dsimproc.lean
iterators.lean
james1.lean
james1.lean.out.expected
jason1.lean
jpCasesDiscrM.lean
jpCasesDiscrM.lean.out.expected
jpCasesNary.lean
jpCasesNary.lean.out.expected
jpClosureIssue.lean
jpClosureIssue.lean.out.expected
jpVoidArgs.lean
json.lean
json.lean.out.expected
json2.lean
json_empty.lean
jsonSurrogates.lean
kernel1.lean
kernel2.lean
kernel_maxheartbeats.lean
kernelBacktrack.lean
kernelBacktrack.lean.out.expected
kernelErrorFollowup.lean
kernelInterrupt.lean
kevin.lean
keyAttrErase.lean
keyAttrErase.lean.out.expected
krivine.lean
kronRWIssue.lean
kronRWIssue.lean.out.expected
KyleAlg.lean feat: beta reduce while elaborating applications (#13807) 2026-05-21 07:26:00 +00:00
KyleAlg.lean.out.expected
KyleAlgAbbrev.lean feat: beta reduce while elaborating applications (#13807) 2026-05-21 07:26:00 +00:00
lambdaLiftCache.lean
lambdaLiftCache.lean.out.expected
lazyListRotateUnfoldProof.lean
lazyListRotateUnfoldProof.lean.out.expected
lazylistThunk.lean
lazySeq.lean
lazySeq.lean.out.expected
lazyUnfoldingPerfIssue.lean
lazyUnfoldingPerfIssue.lean.out.expected
lcnf2.lean
lcnf2.lean.out.ignored
lcnf3.lean
lcnf_borrow_expected_type.lean
lcnf_export_borrow_error.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
lcnf_simp_let.lean
lcnfBinderNameBug.lean
lcnfCache.lean
lcnfCache.lean.out.expected
lcnfCastIssue.lean
lcnfCheckIssue.lean
lcnfCheckIssue.lean.out.ignored
lcnfErasure.lean
lcnfInferProjTypeBug.lean
lcnfInferProjTypeBug.lean.out.ignored
lcnfInferProjTypeIssue.lean
lcnfInferProjTypeIssue.lean.out.ignored
lcnfInliningIssue.lean
lcnfInliningIssue.lean.out.ignored
lcnfIssue.lean
lcnfIssue.lean.out.ignored
lcnfTypes.lean
lcnfTypes.lean.out.expected
LE.lean
LE.lean.out.expected
lean3_zulip_issues_1.lean
lean3RefineBug.lean
lean3RefineBug.lean.out.expected
lean_nat_bitwise.lean
lean_nat_gcd.lean
left_right.lean
lemma.lean
let_Issue.lean
letBRecOnIssue.lean
letDeclSimp.lean
letFun.lean
letFun.lean.out.expected
letFunUnusedVarBug.lean
letMVar.lean
letMVar.lean.out.expected
letNonDep.lean
letrecInProofs.lean
letrecInThm.lean
letRecTheorem.lean
letRecTheorem.lean.out.expected
letrecWFIssue.lean
letToHave.lean
letToHaveCleanup.lean
level.lean
levelNamesInTacticMode.lean
levelNGen.lean
levelNGen.lean.out.expected
levenshtein.lean
lex.lean
lia_order_bug.lean
lia_with_cases.lean
liaByRefl.lean
library_search_all.lean
library_search_grind.lean
library_search_grind.lean.out.expected
library_suggestions.lean
library_suggestions.lean.out.ignored
library_suggestions_deprecated.lean
library_suggestions_import.lean
library_suggestions_local.lean
library_suggestions_mepo.lean
library_suggestions_mepo.lean.out.ignored
library_suggestions_mepo_order.lean feat: filter MePo candidates to theorems and order output by iteration (#13750) 2026-05-18 14:15:06 +00:00
library_suggestions_mepo_order.lean.out.expected feat: filter MePo candidates to theorems and order output by iteration (#13750) 2026-05-18 14:15:06 +00:00
library_suggestions_override.lean
library_suggestions_persistent.lean
library_suggestions_persistent_module.lean
library_suggestions_private.lean
library_suggestions_relevant_constants.lean fix: instantiate metavariables when collecting a goal's constants (#13748) 2026-05-18 15:52:13 +00:00
library_suggestions_relevant_constants.lean.out.expected fix: instantiate metavariables when collecting a goal's constants (#13748) 2026-05-18 15:52:13 +00:00
library_suggestions_sine_qua_non.lean
librarySearch.lean
librarySearch.lean.out.expected
libuv.lean
lift_lets.lean
liftMethodInMacrosIssue.lean
LiftMethodIssue.lean
linearByRefl.lean
linearCategory_perf_issue.lean
linearCategory_perf_issue.lean.out.expected
linearDecEq.lean
linearNoConfusion.lean
linterCoe.lean feat: missingDocs linter warns about empty doc strings (#13188) 2026-03-30 19:48:25 +00:00
linterMissingDocs.lean feat: add linter.redundantVisibility for redundant private/public modifiers (#13132) 2026-04-13 08:34:20 +00:00
linterMissingDocs.lean.out.expected feat: add linter.redundantVisibility for redundant private/public modifiers (#13132) 2026-04-13 08:34:20 +00:00
linterRedundantExpose.lean feat: add warn.redundantExpose for redundant @[expose]/@[no_expose] attributes (#13359) 2026-04-27 10:33:58 +00:00
linterSuspiciousUnexpanderPatterns.lean
linterSuspiciousUnexpanderPatterns.lean.out.expected
linterTacticCheckInstances.lean feat: add .instances-transparency type-check diagnostics (#13368) 2026-05-02 12:17:51 +00:00
linterUnusedDecidableInType.lean feat: upstream unusedDecidableInType linter (#13688) 2026-05-14 11:56:22 +00:00
list_monadic_functions.lean
list_monadic_functions.lean.out.expected
list_simp.lean
list_variables_linter.lean fix: do not modify infotrees in withSetOptionIn (#11313) 2026-05-11 11:36:39 +00:00
listDecEq.lean
listLength.lean
listLength.lean.out.expected
listtostring.lean
listtostring.lean.out.expected
lit_values.lean
lit_values.lean.out.expected
litToCtor.lean
localGlobalNotation.lean
localNameResolutionWithProj.lean
localNotationPP.lean
localNotationPP.lean.out.expected
localParsers.lean
lossy_casts.lean
lrat_roundtrip.lean
lvl1.lean
lvl1.lean.out.expected feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
macro.lean
macro2.lean
macro3.lean
macro_macro.lean
macro_macro.lean.out.expected
macroElabRulesIssue1.lean
macroElabRulesIssue1.lean.out.expected
macroid.lean
macroid.lean.out.expected
macroParams.lean
macroResolveName.lean
macroResolveName.lean.out.expected
macroscopes.lean
macroscopes.lean.out.expected
macroTrace.lean
macroTrace.lean.out.expected
magical.lean
mainIncorrectType1.lean
mainIncorrectType2.lean
mainIncorrectType3.lean
mainIncorrectType4.lean
mainIncorrectType5.lean
mainType1.lean
mainType2.lean
mainType3.lean
mainType4.lean
mainType5.lean
mainType6.lean
mangling.lean
manyAritySyntax.lean
mapTR.lean
match1.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
match2.lean
match2.lean.out.ignored
match3.lean
match3.lean.out.expected
match4.lean
match4.lean.out.expected
match_ctorIdx.lean
match_eqns_bug.lean
match_expose_implicit_reducible.lean feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
match_expr.lean
match_expr_expected_type_issue.lean
match_expr_meta_modifier.lean
match_expr_perf.lean feat: efficient tactic configuration elaborators and configurability (#13651) 2026-05-14 17:20:57 +00:00
match_int_lit_issue.lean
match_lit_fin_cover.lean
match_lit_issues.lean
match_lit_issues.lean.out.expected
match_lit_regression.lean
match_lit_regression.lean.out.expected
match_nat.lean feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
match_unit.lean
matchApp.lean
matchApp.lean.out.expected
matchArrayLit.lean
matchCongrEqns.lean
matchDiscrType.lean
matchEqnsHEqIssue.lean
matchEqnsHEqIssue.lean.out.expected
matchEqs.lean
matchEqs.lean.out.expected
matchEqsBug.lean
matchEqsBug.lean.out.expected
matcherElimUniv.lean
matchGenBug.lean
matchGenBug.lean.out.expected
matchGenIssue.lean
matchMissingCase.lean fix: show missing match cases in declaration order (#13266) 2026-04-03 13:33:54 +00:00
matchMultAlt.lean
matchMultAlt.lean.out.expected
matchNoPostponing.lean
matchOfNatIssue.lean
matchOfNatIssue.lean.out.expected
matchPatternInsideBinders.lean
matchPatternInsideBinders.lean.out.expected
matchPatternPartialApp.lean
matchPatternPartialApp.lean.out.expected
matchPatternVarErrors.lean
matchRw.lean
matchSparse.lean feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
matchSparse2.lean
matchtac.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
matchtac.lean.out.expected
matchUnifyBug.lean
matchunit.lean
matchunit.lean.out.expected
matchVarIssue.lean
matchWithSearch.lean
mathlibetaissue.lean
mathlibetaissue.lean.out.expected
mathport18.lean
mathport18.lean.out.expected
mathport_issue16.lean
mathport_issue16.lean.out.expected
matrix.lean
maxSuggestionsTest.lean
may_postpone_tc.lean
maze.lean
mergeSort.lean
mergeSortCPDT.lean
messageKind.lean
meta.lean fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
meta1.lean
meta2.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
meta2.lean.out.ignored
meta3.lean
meta4.lean
meta5.lean
meta6.lean
meta6.lean.out.expected
meta7.lean
meta7.lean.out.ignored
methodSpecs.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
methodSpecsDeriving.lean
methodsRetInhabited.lean
mightBeDerivable.lean
Miller1.lean
mintroErrorMessage.lean
missingDeclName.lean
missingDocsTacticAlt.lean
missingExplicitWithForwardNamedDep.lean
missingSizeOfArrayGetThm.lean
mixedMacroRules.lean
mixedMacroRules.lean.out.expected
mixfix.lean
mjissue.lean
modAsClasses.lean
moduleDoc.lean
moduleDoc.lean.out.expected
moduleHeaderLeadingWhitespace.lean
monadCache.lean
monadCache.lean.out.expected
monadControl.lean
MonadControl_tutorial.lean
monotone.lean
more_jps.lean
mspecInvariantInstantiation.lean
mspecInvariantInstantiation.lean.out.expected
mspecNoAssignSyntheticOpaque.lean
mul_match_pattern.lean
mulcomm.lean
multiTargetCasesInductionIssue.lean
mut_ind_wf.lean
mutual_coinduction.lean
mutual_termination_by_errors.lean
mutualDefThms.lean
mutualWithCompositeNames.lean
mutualWithMacro.lean
mutualWithNamespaceMacro.lean
mutwf1.lean
mutwf2.lean
mutwf2.lean.out.expected
mutwf3.lean
mutwf3.lean.out.expected
mutwf4.lean
mutwf4.lean.out.expected
mvar_fvar.lean
mvar_fvar.lean.out.expected
mvcgenInvariantsSuggestions.lean
mvcgenInvariantsWith.lean
mvcgenJPs.lean
mvcgenLocalSpec.lean
mvcgenPRangeInst.lean
mvcgenRflReducibility.lean
mvcgenSimpClassMethod.lean
mvcgenSplitState.lean
mvcgenTutorial.lean feat: use explicit allowlist instead of transparency bump in whnfMatcher (#13363) 2026-04-24 13:50:30 +00:00
mvcgenUnknownIdent.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
mvcgenWithFail.lean
name_eq_bug.lean
namelit.lean
namelit.lean.out.expected
namePatEqThm.lean
nameRepr.lean
nameRepr.lean.out.expected
namespaceHyg.lean
namespaceIssue.lean
namespaceResolution.lean
nary_nomatch.lean
nat_mod_defeq.lean
nativeReflBackdoor.lean
natlit.lean
negFloat.lean
negFloat.lean.out.expected
nested_inductive.lean
nested_match_bug.lean
nested_match_slowdown.lean fix: show missing match cases in declaration order (#13266) 2026-04-03 13:33:54 +00:00
nestedDo.lean
nestedInductiveConstructions.lean
nestedInductiveIssue.lean
nestedInductiveRecType.lean
nestedInductiveUniverse.lean
nestedIssueMatch.lean
nestedIssueMatch.lean.out.expected
nestedrec.lean
nestedtc.lean
nestedtc.lean.out.expected
nestedTypeFormers.lean
nestedWF.lean
nestedWF.lean.out.expected
net_addr.lean
networkInterfaces.lean
never_extract.lean
new_compiler.lean
new_frontend2.lean
new_frontend2.lean.out.expected
new_inductive.lean
new_inductive.lean.out.expected
new_inductive2.lean
new_inductive2.lean.out.expected
newdo.lean chore: remove repeat/while macro_rules bootstrap from Init.While (#13479) 2026-04-19 21:01:14 +00:00
newdo.lean.out.expected
newfrontend1.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
newfrontend1.lean.out.expected
newfrontend2.lean
newfrontend2.lean.out.expected
newfrontend3.lean
newfrontend3.lean.out.expected
newfrontend5.lean
newfrontend5.lean.out.expected
nicerNestedDos.lean
no_grind_constProp.lean
no_grind_constProp.lean.out.ignored
no_simproc_usize.lean
no_simproc_usize.lean.out.expected
noConfusionCtorInjection.lean fix: missing proof hints in grind propagators (#13623) 2026-05-03 14:51:03 +00:00
noConfusionCtors.lean
noErrorUtil.lean
noFallbackAttr.lean feat: add [no_fallback] attribute for tactic elaborators and macros (#13523) 2026-04-26 13:59:54 +00:00
nofun1.lean
noindexAnnotation.lean
nomatch_regression.lean
nomatch_tac.lean
nonClassInstance.lean feat: better error messages and more complete logic for checkImpossibleInstance and checkNonClassInstance (#13550) 2026-05-14 09:40:03 +00:00
noncomp.lean
noncompSection.lean
noncompSection.lean.out.expected
noncomputable_bug.lean
noncomputable_decide.lean
noncomputableUnused.lean
nondepArrow.lean
nondepArrow.lean.out.expected
nonrec.lean
norm_cast.lean
notationDelab.lean
notationDelab.lean.out.expected
numChars.lean
obtain.lean
offsetIssue.lean
ofNat_class.lean
ofNatNormNum.lean
ofNatNormNum.lean.out.expected
omega.lean
omega_examples.lean
omegaCanon.lean
omegaDischarger.lean
omegaDischarger.lean.out.expected
opaqueCodeGen.lean
openInScopeBug.lean
openTermTactic.lean
optionDecEq.lean
optionGetD.lean
optionGetD.lean.out.expected
optParam.lean
or_shortcircuit.lean
or_shortcircuit.lean.out.expected
Ord.lean
order.lean
order.lean.out.expected
overAndPartialAppsAtWF.lean
overAndPartialAppsAtWF.lean.out.expected
overlappingTokens.lean
overloaded.lean
overloaded.lean.out.expected
overloadsAndDelayedCoercions.lean
pairsSumToZero.lean
pairsSumToZero.lean.out.expected
panicAtCheckAssignment.lean
parray1.lean
PArray_forM.lean
PArray_forM.lean.out.expected
parseEnd.lean
parsePrelude.lean
parsePrelude.lean.out.expected
parserAliasShadow.lean
parserQuot.lean
parserQuot.lean.out.expected
partial1.lean
partial1.lean.out.expected
partial_fixpoint.lean
partial_fixpoint_aeneas.lean
partial_fixpoint_aeneas2.lean
partial_fixpoint_aeneas2.lean.out.expected
partial_fixpoint_explicit.lean
partial_fixpoint_f91.lean
partial_fixpoint_induct.lean
partial_fixpoint_monadic.lean
partial_fixpoint_monotonicity.lean
partial_fixpoint_mutual.lean
partial_fixpoint_probability.lean
partial_fixpoint_prop.lean
partial_fixpoint_split.lean
partialApp.lean
partialDelta.lean
patbug.lean
patternInvalidNamedArg.lean
pendingInstBug.lean
pendingMVarIssue.lean
persistent_lint_log.lean feat: lake: add support for running text linters from lake lint (#13513) 2026-04-28 15:09:04 +00:00
phashmap_iter.lean
postponeBinRelIssue.lean
posView.lean
pow_exploit.lean
ppBeta.lean
ppBeta.lean.out.expected
ppDeepTerms.lean
ppDeepTerms.lean.out.expected
ppExpr.lean
ppExpr.lean.out.expected
ppFVarsAnonymous.lean
PPInstances.lean
PPInstances.lean.out.expected
ppite.lean
ppite.lean.out.expected
ppLet.lean
pplevel.lean
pplevel.lean.out.expected
ppMaxSteps.lean
ppMData.lean
ppMotives.lean
ppMotives.lean.out.expected
ppMVars.lean feat: pretty print level metavariables using index (#13030) 2026-04-01 22:34:29 +00:00
ppMVarsDocstrings.lean feat: informative metavariable hovers, better delayed assignment pretty printing (#13446) 2026-04-23 01:43:55 +00:00
ppNotationCode.lean
ppNotationCode.lean.out.expected
ppNumericTypes.lean
ppOneline.lean
ppParens.lean
ppPiBinderNames.lean
PProd_syntax.lean
PPRoundtrip.lean
PPRoundtrip.lean.out.expected
ppSpaces.lean
ppSyntax.lean
ppSyntax.lean.out.expected
PPTopDownAnalyze.lean
PPTopDownAnalyze.lean.out.expected
ppUnicode.lean
ppUniverses.lean fix: pp.universes should not affect constants with no universe levels (#13761) 2026-05-17 01:41:04 +00:00
ppUsingAnonymousConstructor.lean
ppVector.lean
precDSL.lean
precDSL.lean.out.expected
prefixTableStep.lean
prelude-injectivity.lean
primProjEtaIssue.lean
primProjEtaIssue.lean.out.expected
print_cmd.lean
print_cmd.lean.out.expected
printEqns.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
printPrivate.lean
printStructure.lean refactor: make CancelToken Promise-based (#13303) 2026-04-28 21:50:54 +00:00
prioDSL.lean
privateCtor.lean
privateFieldCopyIssue.lean
privateFieldCopyIssue.lean.out.expected
privateInPublic.lean
Process.lean
Process.lean.out.expected
processGenDiseqBug.lean
proj_delta_issue.lean
projDefEq2.lean
projWithIrrelevantFields.lean
projWithNestedIrrelevantFields.lean
promise.lean
proofAsSorry.lean
proofDataConfusionBug.lean
proofIrrelFVar.lean
propagateExpectedType.lean
prv.lean
prv.lean.out.expected
prvNameWithMacroScopes.lean
psumAtWF.lean
ptrAddr.lean
ptrAddr.lean.out.ignored
qed_macro.lean
qualifiedNamesRec.lean
quasi_pattern_unification_approx_issue.lean
quotInd.lean
quotInd.lean.out.expected
range.lean
rangePolymorphic.lean
Rat.lean
rat1.lean
rat1.lean.out.expected
rational.lean
rational.lean.out.expected
rawStrings.lean
rc_tests.lean
rcases.lean
rcases1.lean
readDir.lean
readDir.lean.out.expected
readerThe.lean
realPath.lean
realPath.lean.out.ignored
recCommonPrefixAlpha.lean
recconstructorcrash.lean
recInfo1.lean
recommendedSpelling.lean
reduce1.lean
reduce2.lean
reduce3.lean
reduce3.lean.out.expected
reduceArity.lean
reduceArity.lean.out.expected
reduceBEqSimproc.lean refactor: use Nat.decEq in derived BEq instances (#13390) 2026-04-13 15:24:04 +00:00
reduceBool.lean
reduceBool.lean.out.expected
reduceCtorIdxSimproc.lean
reducibilityAttrValidation.lean
reducibleClassField_perf.lean
reductionBug.lean
redundantDeprecatedWarnings.lean feat: remove redundant deprecation warnings (#13595) 2026-05-07 15:43:34 +00:00
redundantVisibility.lean feat: add linter.redundantVisibility for redundant private/public modifiers (#13132) 2026-04-13 08:34:20 +00:00
ref1.lean
ref1.lean.out.expected
refl.lean
reflectiveIndPred.lean
reflectiveIndPred.lean.out.expected
Reformat.lean
Reformat.lean.input
Reformat.lean.out.expected
regressions3210.lean
Reid1.lean
Reid1.lean.out.expected
renameI.lean
renameI.lean.out.expected
renameI2.lean
renameI2.lean.out.expected
renameSelf.lean
renaming.lean
repeat.lean
repeatConv.lean
replace.lean
replace.lean.out.expected
replace_tac.lean
replayConst.lean
repr.lean
repr.lean.out.expected
repr_empty.lean
repr_issue.lean
repr_issue.lean.out.expected
reprove.lean
reserved.lean
reservedNameResolution.lean
resolveGlobalName.lean
resolveGlobalName.lean.out.expected
resolveLVal.lean
returnOptIssue.lean
revert1.lean
revertlet.lean
revertlet.lean.out.expected
revertMetavarKind.lean
rewrite.lean feat: add warning when applying global attribute using in (#13223) 2026-04-08 06:20:34 +00:00
rewrites.lean
rfl_simp_thm.lean
rfl_simp_thm.lean.out.expected
rflApplyFoApprox.lean
rflApplyFoApprox.lean.out.expected
rflProofsCongrCastsIssue.lean
rflReducibility.lean
rflTacticErrors.lean fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
robinson.lean
robinson.lean.out.expected
root.lean
root.lean.out.expected
rossel1.lean
rossel1.lean.out.expected
run_cmd.lean
run_meta1.lean
run_test.sh chore: fixes from #13103 "enable separate codegen" (#13241) 2026-04-02 11:13:22 +00:00
runSTBug.lean
runSTBug.lean.out.expected
rw_inst_implicit_args.lean
rw_inst_mvars.lean
rwEqThms.lean
rwEqThms.lean.out.expected
rwPrioritizesLCtxOverEnv.lean
rwRegression.lean
rwWithElabError.lean
safeExp.lean
safeShadowing.lean
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.out.expected
sarray.lean
sarray.lean.out.ignored
scc.lean
scopeCacheProofs.lean
scopedCommandAfterOpen.lean
scopedCommandAfterOpen.lean.out.expected
scopedHindingIssue.lean
scopedHindingIssue.lean.out.expected
scopedLocalReducibility.lean
scopedParsers.lean
scopedParsers.lean.out.expected
scopedParsers2.lean
scopedParsers2.lean.out.expected
scopedunifhint.lean
scopedunifhint.lean.out.expected
sealCommand.lean
secVarBug.lean
secVarBug.lean.out.expected
sepByIndentQuot.lean
sepByIndentQuot.lean.out.expected
seqToCodeIssue.lean
seqToCodeIssue.lean.out.expected
set.lean
set_lit_unexpand.lean
setOptionErrors.lean
setOptionTermTactic.lean
setOptionTermTactic.lean.out.expected
setStructInstNotation.lean
seval1.lean
sharecommon.lean
sharecommon_mpz.lean
show_term.lean
showTactic.lean
showTests.lean
shrinkFn.lean
sigmaprec.lean
sign.lean
simp-elab-recover.lean
simp1.lean
simp1.lean.out.ignored
simp2.lean
simp3.lean
simp4.lean
simp5.lean
simp6.lean
simp_all.lean
simp_all_contextual.lean
simp_all_duplicateHyps.lean
simp_all_duplicateHyps.lean.out.expected
simp_arith_deprecated.lean
simp_arith_issues.lean
simp_arith_issues.lean.out.expected
simp_cache_perf_issue.lean
simp_cache_perf_issue.lean.out.expected
simp_cases.lean
simp_dsimp.lean
simp_dsimp.lean.out.expected
simp_eqn_bug.lean
simp_failIfUnchanged.lean
simp_inst_implict_args.lean
simp_int_arith.lean
simp_locals.lean
simp_locals_module.lean
simp_nat_arith.lean
simp_proj_transparency_issue.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
simp_reducibleClassField.lean
simp_rfl_check_transparency.lean fix: suggest (rfl) not id rfl in linter (#13319) 2026-04-08 08:21:23 +00:00
simp_suggestions.lean
simp_trace_backtrack.lean
simp_trace_backtrack.lean.out.expected
simpArith1.lean
simpArith1.lean.out.expected
simpArithCacheIssue.lean
simpArrayIdx.lean
simpAtDefIssue.lean
simpAutoUnfold.lean
simpBool.lean
simpBug.lean
simpCacheTest.lean
simpCasesOnCtorBug.lean
simpCasesOnCtorBug.lean.out.ignored
simpcfg.lean
simpcfg.lean.out.expected
simpCnstr1.lean
simpCondLemma.lean
simpConfigPropagationIssue1.lean
simpConfigPropagationIssue3.lean
simpDecide.lean
simpDefToUnfold.lean
simpDiag.lean
simpDiag.lean.out.expected
simpDisch.lean
simpDisch.lean.out.expected
simpDischargeLoop.lean
simpDischargeLoop.lean.out.expected
simpExtraArgsBug.lean
simpExtraArgsBug.lean.out.expected
simpGround1.lean
simpGround1.lean.out.expected
simpHave.lean
simpHigherOrder.lean
simpIfPre.lean
simpImpLocal.lean
simpIndexDiag.lean
simpIndexDiag.lean.out.expected
simpInv.lean
simpIssue.lean
simpJpCasesDepBug.lean
simple_ground_extraction.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
simple_reuse.lean
simpLetFunIssue.lean
simpLoopBug.lean
simpLoopProtection.lean
simpMatch.lean
simpMatchDiscr.lean
simpMatchDiscr.lean.out.expected
simpMatchDiscrIssue.lean
simpMatchEta.lean
simpOnly.lean
simpPartialApp.lean
simpPartialApp.lean.out.expected
simpPrefixIssue.lean
simpPrefixIssue.lean.out.expected
simpPreIssue.lean
simpPreprocess.lean
simpPreprocess.lean.out.expected
simpPrio.lean
simproc1.lean
simproc2.lean
simproc_builtin_erase.lean
simproc_disable_issue.lean
simproc_disable_issue.lean.out.expected
simproc_erase.lean
simproc_panic.lean
simproc_timeout.lean
simproc_timeout.lean.out.expected
simprocChar.lean
simprocChar.lean.out.expected
simprocDigitChar.lean
simprocEval1.lean
simprocEval1.lean.out.expected
simprocEval2.lean
simprocEval2.lean.out.expected
simprocEval3.lean
simprocEval3.lean.out.expected
simprocEval4.lean
simprocEval4.lean.out.expected
simprocFin.lean
simprocNat.lean
simprocSInt.lean
simprocString.lean
simprocTrace.lean
simprocTrace.lean.out.expected
simprocUInt.lean
simpRwBug.lean
simpSInt.lean
simpStar.lean
simpStarHyp.lean
simpTrace.lean
simpTracePostIssue.lean
simpTracePostIssue.lean.out.expected
simpUnfoldAbbrev.lean
simpUnusedArgs.lean
simpVarHead.lean chore: enable warning.simp.varHead (#13403) 2026-04-16 16:11:09 +00:00
simpZetaFalse.lean
simpZetaFalse.lean.out.expected
sint-abs.lean
sint_basic.lean
sint_basic.lean.out.expected
sint_conversions.lean
sint_div_overflow.lean
sint_div_overflow.lean.out.expected
sizeof.lean
sizeof.lean.out.expected
sizeof1.lean
sizeof1.lean.out.expected feat: no [defeq] attribute on sizeOf_spec lemmas (#13320) 2026-04-08 11:10:50 +00:00
sizeof2.lean
sizeof2.lean.out.expected
sizeof3.lean
sizeof3.lean.out.expected feat: no [defeq] attribute on sizeOf_spec lemmas (#13320) 2026-04-08 11:10:50 +00:00
sizeof4.lean
sizeof4.lean.out.expected
sizeof5.lean
sizeof5.lean.out.expected
sizeof6.lean
sizeof6.lean.out.expected
skipAssignedInstances.lean
skipKernelTC.lean
slice.lean
smartUnfolding.lean
smartUnfolding.lean.out.expected
smartUnfoldingBug.lean
smartUnfoldingMatch.lean
smartUnfoldingMatch.lean.out.expected
snapshotTree.lean
snapshotTree.lean.out.expected
solve_by_elim.lean feat: add warning when applying global attribute using in (#13223) 2026-04-08 06:20:34 +00:00
solve_by_elim_suggestions.lean
som1.lean
sorry.lean
sorryWarning.lean
sorryWarning.lean.out.expected
sparseCasesOn.lean chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +00:00
spec_issue.lean
spec_issue.lean.out.expected
spec_limit.lean
specbug.lean
specFixedHOParamModuloErased.lean
specialize1.lean feat: MVarId.assertAfter fvar alias info, MVarId.replace mvar dependencies, specialize tactic using eta arguments (#13528) 2026-04-30 10:36:29 +00:00
specialize2.lean
specialize3.lean
specialize_cache_miscompile.lean
specInvariantAttr.lean
split1.lean
split2.lean
split3.lean
split_mvars_target.lean
splitAtCode.lean
splitErrors.lean
splitIfIssue.lean
splitIfIssue.lean.out.expected
splitIssue.lean
splitIssue.lean.out.expected
splitIssue2.lean
splitIssue2.lean.out.expected
splitIssue3.lean
splitIssue3.lean.out.expected
splitList.lean
splitList.lean.out.expected
splitOrderIssue.lean
spredNotation.lean
spredProofMode.lean
st_test.lean
starsAndBars.lean
state8.lean
state12.lean
stateRef.lean
stdDoPostUnit.lean
stdio.lean
stdio.lean.before.sh
stdio.lean.out.expected
stream.lean
stream.lean.out.expected
streamEqIssue.lean
streamEqIssue.lean.out.expected
strictImplicit.lean
strictImplicit.lean.out.expected
string.lean
string_cases.lean fix: correct String cases codegen to use String.toByteArray (#13242) 2026-04-02 08:17:20 +00:00
string_cases.lean.out.expected fix: correct String cases codegen to use String.toByteArray (#13242) 2026-04-02 08:17:20 +00:00
string_gaps.lean
string_imp.lean
string_imp.lean.out.expected
string_imp2.lean
string_imp2.lean.out.expected
string_kmp.lean
string_neq_kernel_cost.lean
string_pos_grind.lean
string_replace.lean
string_simprocs.lean
string_slice.lean
string_termination.lean
string_toNat_underscores.lean
strInterpolation.lean
strInterpolation.lean.out.expected
strLitProj.lean
strLitProj.lean.out.expected
struct1.lean
struct1.lean.out.expected
struct2.lean
struct2.lean.out.expected
struct3.lean
struct_inst_typed.lean
struct_instance_in_eqn.lean
structBinderIdent.lean
structBinderUpdates.lean
structEqns.lean
structInst.lean
structInst2.lean
structInst3.lean
structInst4.lean
structInstExtraEta.lean
structInstFast.lean
structInstSourcesLeftToRight.lean
structInstSourcesLeftToRight.lean.out.expected
structInstUpdates.lean
structNamedParentProj.lean
structNoBody.lean
structPrivateFieldBug.lean
structPrivateFieldBug2.lean
structuralEqn6.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
structuralEqns.lean
structuralEqns.lean.out.expected
structuralEqns2.lean
structuralEqns2.lean.out.expected
structuralEqns3.lean
structuralEqns3.lean.out.expected
structuralEqns4.lean
structuralEqns5.lean
structuralIssue.lean
structuralIssue2.lean
structuralMutual.lean
structuralNamedF.lean
structuralOverNested.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
structuralRec1.lean
structuralRec2.lean
structure.lean
structure_recursive.lean
structureElab.lean
structWithAlgTCSynth.lean
structWithAlgTCSynth.lean.out.expected fix: wrapInstance should not reduce non-constructor instances (#13327) 2026-04-08 16:31:28 +00:00
stuckMVarBug.lean
stuckMVarBug.lean.out.expected
stuckTC.lean
stxKindInsideNamespace.lean
stxKindInsideNamespace.lean.out.expected
stxMacro.lean
stxMacro.lean.out.expected
subarray_split.lean
subexpr.lean
subscript_parser.lean
subset.lean
subset.lean.out.expected
subsingletonCasesOn.lean
subst.lean
subst1.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
subst1.lean.out.ignored
substlet.lean
substVars.lean
substWithoutExpectedType.lean
subtype_inj.lean
suffices.lean
sym_arith_classify.lean feat: add Sym.Arith infrastructure for arithmetic normalization (#13289) 2026-04-06 05:21:09 +00:00
sym_arith_reify.lean feat: add Sym.Arith infrastructure for arithmetic normalization (#13289) 2026-04-06 05:21:09 +00:00
sym_cbv_12336.lean
sym_congrInfo.lean
sym_discrtree_eta.lean
sym_eta_mwe.lean fix: eta-reduce patterns containing loose pattern variables (#13448) 2026-04-17 20:49:21 +00:00
sym_getMaxFVar.lean
sym_instantiate.lean
sym_interactive1.lean
sym_interactive_bugs.lean fix: prune goals assigned by isDefEq in sym => mode (#13474) 2026-04-19 11:55:11 +00:00
sym_intro.lean
sym_intro_have.lean
sym_intro_issue.lean fix: avoid assigning mvar when Sym.intros produces no binders (#13451) 2026-04-17 21:47:47 +00:00
sym_issue_13416.lean test: add regression test for Sym.simp eta-reduction (#13416) (#13452) 2026-04-17 22:47:53 +00:00
sym_liftLower.lean
sym_pattern.lean
sym_pattern_2.lean fix: eta-reduce patterns containing loose pattern variables (#13448) 2026-04-17 20:49:21 +00:00
sym_pattern_3.lean
sym_pattern_level.lean
sym_pattern_universe_issue.lean fix: missing case in processLevel at SymM (#13612) 2026-05-02 17:52:43 +00:00
sym_proj_issue.lean fix: kernel projection panic in Sym.simp match reduction (#13635) 2026-05-05 03:20:20 +00:00
sym_register_variant1.lean
sym_simp_1.lean fix: eta-reduce patterns containing loose pattern variables (#13448) 2026-04-17 20:49:21 +00:00
sym_simp_2.lean
sym_simp_3.lean chore: minor tweaks to Sym.simp test and benchmark (#13468) 2026-04-18 21:11:30 +00:00
sym_simp_4.lean
sym_simp_5.lean
sym_simp_adapt1.lean
sym_simp_cd.lean
sym_simp_cd_unit.lean
sym_simp_dsl_control1.lean
sym_simp_interactive1.lean
sym_simp_perm1.lean
sym_simp_set.lean
sym_simproc_dsl1.lean
symbolFrequency.lean
symbolFrequency_foldRelevantConsts.lean
symm.lean
sync_barrier.lean
sync_channel.lean
sync_mutex.lean
sync_notify.lean refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +00:00
sync_recursive_mutex.lean
sync_shared_mutex.lean
syntax1.lean
syntax1.lean.out.expected
syntaxAbbrevQuot.lean
syntaxAbbrevQuot.lean.out.expected
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.out.expected
syntaxPrio.lean
syntaxPrio.lean.out.expected
synth1.lean
synth1.lean.out.expected
syntheticOpaqueReadOnly.lean
syntheticOpaqueReadOnly.lean.out.expected
synthInstsIssue.lean
synthInstsIssue.lean.out.expected
synthOrderRegression.lean
synthOrderRegression.lean.out.expected
synthPending1.lean
synthPendingBug.lean
tabulate.lean
tabulate.lean.out.expected
tactic.lean
tactic1.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
tactic1.lean.out.expected
tactic_config.lean feat: efficient tactic configuration elaborators and configurability (#13651) 2026-05-14 17:20:57 +00:00
tacticDoc.lean
tacticDocAllModule.lean
tacticDocAllNonmod.lean
tacticDocUserName.lean
tacticExtOverlap.lean
tacticTests.lean
tagged_return_1.lean
tagged_return_2.lean
takeSimpEqns.lean
task_iterators.lean
task_test.lean
task_test.lean.out.ignored
task_test2.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
task_test2.lean.out.ignored
task_test_io.lean
task_test_io.lean.out.expected
taskState.lean
tc_cache.lean
tc_eta_struct_issue.lean
tc_eta_struct_issue.lean.out.expected
tcUnivIssue.lean
tempfile.lean
termElab.lean
terminalAsSorry.lean
terminalAsSorry.lean.out.expected
termination_by_where.lean
terminationByStructurally.lean
termParserAttr.lean
TermSeq.lean
test_binary_dec_proc_fold.lean
test_proj_hints.lean
test_simp_reducible_class.lean feat: add instance validation checks in addInstance (#13389) 2026-04-16 17:48:16 +00:00
thmIsProp.lean
thmsOpaque.lean
thunk.lean
thunk.lean.out.expected
thunkTaskCasesOn.lean
time.lean
timeAPI.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeCanonFormats.lean
timeClassOperations.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeFormats.lean feat: add Locale and LocaleSymbols for configurable date/time formatting (#13567) 2026-05-12 13:21:25 +00:00
timeIO.lean
timeLimits.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeLocalDateTime.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeNegative.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeOperations.lean
timeOperationsOffset.lean
timeParse.lean feat: add WallTime and simplify Timestamp API (#13675) 2026-05-11 23:26:19 +00:00
timeSet.lean
timeSub.lean
timeTzifParse.lean
to_array_csimp.lean
toArrayEq.lean
toDeclEtaBug.lean
toExpr.lean
toExpr.lean.out.expected
toExpr2.lean
toExpr2.lean.out.expected
toFieldNameIssue.lean
toFieldNameIssue.lean.out.expected
toFromJson.lean
tojson_fromjson_perf_issue.lean
toLCNFCacheBug.lean
toLCNFCacheBug.lean.out.ignored
trace.lean
trace_synth.lean
traceClassScopes.lean
traceClassScopes.lean.out.expected
traceElabIssue.lean
traceFormat.lean
traceStateBacktracking.lean
traceStateBacktracking.lean.out.expected
traceTacticSteps.lean
traceTacticSteps.lean.out.expected
trackZetaDeltaCacheIssue.lean
trans.lean
trans.lean.out.expected
treeMap.lean
treeMap2.lean
treeNode.lean
trivial_uint.lean
try_eval_suggest.lean feat: add try? => tac syntax and parallel cancellation test (#13301) 2026-04-28 10:00:35 +00:00
try_first_par.lean
try_heartbeats.lean
try_induction.lean
try_library_suggestions.lean
try_panic.lean
try_parallelism.lean
try_prelude.lean feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
try_register_builtin.lean
try_solve_by_elim.lean
try_solve_by_elim.lean.out.expected
try_user_suggestions.lean
tryHeuristicPerfIssue.lean
tryHeuristicPerfIssue.lean.out.expected
tryHeuristicPerfIssue2.lean
tryHeuristicPerfIssue2.lean.out.expected
tryOnEmptyBy.lean feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
tryPostponeIssue.lean
type_as_hole.lean
type_class_performance1.lean
type_class_performance1.lean.out.expected
typeAscImp.lean
typeCheckNote.lean feat: add .instances-transparency type-check diagnostics (#13368) 2026-05-02 12:17:51 +00:00
typeclass_append.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
typeclass_append.lean.out.expected
typeclass_coerce.lean
typeclass_coerce.lean.out.expected
typeclass_diamond.lean
typeclass_easy.lean
typeclass_easy.lean.out.expected
typeclass_loop.lean
typeclass_metas_internal_goals1.lean
typeclass_metas_internal_goals2.lean
typeclass_metas_internal_goals3.lean
typeclass_metas_internal_goals4.lean
typeclass_outparam.lean
typeOccursCheckIssue.lean
ubscalar.lean
ubscalar.lean.out.ignored
ugetBorrowed.lean
uintCtors.lean
uintCtors.lean.out.expected
uintMatch.lean
uintMatch.lean.out.expected
unboxStruct.lean
unboxStruct.lean.out.expected
unexpander.lean
unexpander.lean.out.expected
unexpandersNamespaces.lean
unexpandersNamespaces.lean.out.expected
UnexpandSubtype.lean
UnexpandSubtype.lean.out.expected
unexpected_result_with_bind.lean
unfold1.lean
unfold1.lean.out.expected feat: use explicit allowlist instead of transparency bump in whnfMatcher (#13363) 2026-04-24 13:50:30 +00:00
unfold_reducible_class_proj.lean
unfoldDefEq.lean
unfoldDefEq.lean.out.expected
unfoldLemma.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
unfoldMany.lean
unfoldPartialRegression.lean
unfoldr.lean
unfoldReduceMatch.lean
unfoldReduceMatch.lean.out.expected
unfoldTactic.lean
unhygienic.lean
unhygienic.lean.out.expected
unhygienicCode.lean
unhygienicCode.lean.out.expected
unif_issue.lean
unif_issue.lean.out.expected
unif_issue2.lean
unif_issue2.lean.out.expected
unifhint1.lean
unifhint2.lean
unifhint3.lean
unifHintAndTC.lean
unifHintAndTC.lean.out.expected
unihint.lean
unihint.lean.out.expected
univ_out_params.lean
univCnstrApprox.lean
univCnstrApprox.lean.out.expected
univIssue.lean
univParamIssue.lean
univPolyEnum.lean
unlock_limits.lean feat: add unlock_limits command to disable all resource limits (#13211) 2026-04-01 09:26:13 +00:00
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.out.expected
unsafeConst.lean
unsafeConst.lean.out.expected
unsafeInit.lean
unsafeTerm.lean
unusedLet.lean
unusedLet.lean.out.expected
unusedVarDoMatch.lean
unusedVarDoMWE.lean
unusedWarningAtStructUpdate.lean
update.lean
updateExprIssue.lean
updateExprIssue.lean.out.expected
updateLevelIssues.lean
updateLevelIssues.lean.out.expected
Uri.lean
Uri.lean.out.expected
usesOfNoncomputable.lean
utf8英語.lean
valueOfTerm.lean
varBinderUpdate.lean
variable.lean
versoDocClass.lean
versoDocFirstLineHeader.lean
versoDocIndentedHeader.lean fix: elaborate and render blockquotes in Verso docstrings (#13670) 2026-05-06 23:59:11 +00:00
versoDocMarkdown.lean fix: elaborate and render blockquotes in Verso docstrings (#13670) 2026-05-06 23:59:11 +00:00
versoDocMarkdownRendering.lean fix: elaborate and render blockquotes in Verso docstrings (#13670) 2026-05-06 23:59:11 +00:00
versoDocMetadata.lean
versoDocModuleDeclOnly.lean
versoDocModuleFallback.lean
versoDocModuleGiven.lean fix: always fail on unsolved metavariables after Verso docstring elab (#13574) 2026-05-01 22:34:52 +00:00
versoDocModuleVersoOnly.lean
versoDocNesting.lean
versoDocParseError.lean
versoDocs.lean
versoDocs.lean.out.expected
versoDocsModule.lean fix: enforce proper meta discipline for Verso docstring extensions (#13808) 2026-05-21 05:58:09 +00:00
versoDocSuggestionNoImport.lean
versoDocsWhere.lean
versoDocWarningsErrors.lean
warnSorry.lean
weak_specialize.lean
wf_preprocess.lean
wf_preprocess_leak.lean
wfcomputable.lean
wfEqns1.lean
wfEqns1.lean.out.expected
wfEqns2.lean
wfEqns3.lean
wfEqns4.lean
wfEqns5.lean feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) 2026-04-27 10:07:59 +00:00
wfEqnsIssue.lean
wfForIn.lean
wfirred.lean
wfLean3Issue.lean
wfOmega.lean
wfOverapplicationIssue.lean
wfrec-nat.lean
wfrecUnary.lean
wfrecUnusedLet.lean
wfrecUnusedLet.lean.out.expected
WFRelSearch.lean
wfSum.lean
wfUnfold.lean
wfWithSidecondition.lean
where1.lean
whereCmd.lean feat: efficient tactic configuration elaborators and configurability (#13651) 2026-05-14 17:20:57 +00:00
whereCmdModule.lean feat: add module features to #where command (#13811) 2026-05-21 18:11:43 +00:00
whereFinally.lean
while_extrinsic.lean feat: verifiable repeat/while loops (#13209) 2026-05-07 12:48:42 +00:00
whileRepeat.lean feat: support while let in do blocks via unified condition syntax (#13534) 2026-04-27 09:23:36 +00:00
whnfDelayedMVarIssue.lean
whnfProj.lean
whnfProj.lean.out.expected
WindowsNewlines.lean
with_unfolding_none.lean
withAssignableSyntheticOpaqueBug.lean
withAssignableSyntheticOpaqueBug.lean.out.expected
withLocation.lean
withLocation.lean.out.expected
withReducibleAndInstancesCrash.lean
withReducibleAndInstancesCrash.lean.out.ignored
withSetOptionIn.lean fix: do not modify infotrees in withSetOptionIn (#11313) 2026-05-11 11:36:39 +00:00
withWeakNamespace.lean
withWeakNamespace.lean.out.expected
workspaceSymbols.lean
workspaceSymbols.lean.out.expected
zeroExitPoints.lean
zeroExitPoints.lean.out.ignored
zetaDelta.lean
zetaDeltaFalseDefEqIssue.lean
zetaDeltaIssue.lean
zetaDeltaSet.lean
zetaDeltaSet.lean.out.expected
zetaDeltaTryThisIssue.lean
zetaDSimpIssue.lean
zetaUnused.lean
zipper.lean
zipper.lean.out.expected