Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/expose-array-back/./tests/elab
tree: 5c2014437690aa10c28528a5e679bfabd80d8547 [search]
  1. readDir.lean.dir/
  2. .gitattributes
  3. .gitignore
  4. 10067.lean
  5. 10078.lean
  6. 10078.lean.out.expected
  7. 1016.lean
  8. 1017.lean
  9. 1017.lean.out.expected
  10. 10172.lean
  11. 10172.lean.out.expected
  12. 1018.lean
  13. 10181.lean
  14. 10196.lean
  15. 1020.lean
  16. 1021.lean
  17. 1021.lean.out.expected
  18. 10213.lean
  19. 1022.lean
  20. 10234.lean
  21. 10234.lean.out.expected
  22. 1024.lean
  23. 1024.lean.out.expected
  24. 1025.lean
  25. 1025.lean.out.expected
  26. 1026.lean
  27. 1026.lean.out.expected
  28. 1027.lean
  29. 1027.lean.out.expected
  30. 1029.lean
  31. 102_lean3.lean
  32. 1030.lean
  33. 1037.lean
  34. 1039.lean
  35. 1039.lean.out.expected
  36. 10443.lean
  37. 10475.lean
  38. 1051.lean
  39. 1051.lean.out.expected
  40. 10564.lean
  41. 10577.lean
  42. 1058.lean
  43. 10687.lean
  44. 10687.lean.out.expected
  45. 1074a.lean
  46. 10753.lean
  47. 10771.lean
  48. 108.lean
  49. 1080.lean
  50. 1080.lean.out.expected
  51. 10850.lean
  52. 10934.lean
  53. 1098.lean
  54. 1098.lean.out.expected
  55. 10984.lean
  56. 111.lean
  57. 11115.lean
  58. 1112.lean
  59. 1113.lean
  60. 1113.lean.out.expected
  61. 1113b.lean
  62. 1113b.lean.out.expected
  63. 1118.lean
  64. 1120.lean
  65. 1123.lean
  66. 1124.lean
  67. 1127.lean
  68. 1127.lean.out.expected
  69. 1132.lean
  70. 11322.lean
  71. 11337.lean
  72. 11389.lean
  73. 1143.lean
  74. 11509.lean
  75. 1155.lean
  76. 1156.lean
  77. 1158.lean
  78. 1163.lean
  79. 1163.lean.out.expected
  80. 1168.lean
  81. 11687.lean
  82. 1169.lean
  83. 1171.lean
  84. 1171.lean.out.expected
  85. 11719.lean
  86. 11747.lean
  87. 11773.lean
  88. 11778.lean
  89. 1179b.lean
  90. 1179b.lean.out.expected
  91. 1182.lean
  92. 11823.lean
  93. 1184.lean
  94. 1192.lean
  95. 1193a.lean
  96. 1193b.lean
  97. 1194.lean
  98. 1200.lean
  99. 1202.lean
  100. 12025.lean
  101. 12048.lean
  102. 1206.lean
  103. 121.lean
  104. 12136.lean
  105. 12138.lean
  106. 12172_regression.lean
  107. 12215.lean
  108. 12215.lean.out.expected
  109. 12229.lean
  110. 1224.lean
  111. 1228.lean
  112. 1228.lean.out.expected
  113. 1230.lean
  114. 1230.lean.out.expected
  115. 12334.lean
  116. 1234.lean
  117. 1235.lean
  118. 1235.lean.out.expected
  119. 1236.lean
  120. 1237.lean
  121. 1237.lean.out.expected
  122. 12386.lean
  123. 12457.lean
  124. 1247.lean
  125. 125.lean
  126. 1253.lean
  127. 12559.lean
  128. 12563.lean
  129. 1267.lean
  130. 1267.lean.out.expected
  131. 12676.lean
  132. 1274.lean
  133. 1275.lean
  134. 1275.lean.out.expected
  135. 1279.lean
  136. 1279.lean.out.expected
  137. 1279_simplified.lean
  138. 1279_simplified.lean.out.expected
  139. 12815.lean
  140. 1289.lean
  141. 1289.lean.out.expected
  142. 12897.lean
  143. 1292.lean
  144. 1292.lean.out.expected
  145. 1293.lean
  146. 1298.lean
  147. 1298.lean.out.expected
  148. 1299.lean
  149. 1300.lean
  150. 1302.lean
  151. 13043.lean
  152. 1305.lean
  153. 1308.lean
  154. 1308.lean.out.expected
  155. 1311.lean
  156. 13203.lean
  157. 1321.lean
  158. 1321.lean.out.expected
  159. 13268.lean
  160. 13268.lean.out.expected
  161. 13269.lean
  162. 13313.lean
  163. 1333.lean
  164. 1337.lean
  165. 13371.lean
  166. 13407.lean
  167. 13415.lean
  168. 1342.lean
  169. 1342.lean.out.expected
  170. 13485.lean
  171. 13512.lean
  172. 13581.lean
  173. 1359.lean
  174. 1360.lean
  175. 1361.lean
  176. 1361.lean.out.expected
  177. 1361b.lean
  178. 1361b.lean.out.expected
  179. 1363.lean
  180. 1365.lean
  181. 1367.lean
  182. 1367.lean.out.expected
  183. 1372.lean
  184. 1373.lean
  185. 1374.lean
  186. 1375.lean
  187. 1375.lean.out.expected
  188. 13768.lean
  189. 1377.lean
  190. 1377.lean.out.expected
  191. 13770.lean
  192. 1380.lean
  193. 1380.lean.out.expected
  194. 1385.lean
  195. 1385.lean.out.expected
  196. 1389.lean
  197. 13921.lean
  198. 13929.lean
  199. 13982.lean
  200. 1408.lean
  201. 1408.lean.out.expected
  202. 1411.lean
  203. 1419.lean
  204. 1419.lean.out.expected
  205. 1420.lean
  206. 1426.lean
  207. 1426.lean.out.expected
  208. 1435.lean
  209. 1435.lean.out.expected
  210. 1436.lean
  211. 1441.lean
  212. 1547.lean
  213. 1549.lean
  214. 1558.lean
  215. 1571.lean
  216. 1571.lean.out.expected
  217. 1575.lean
  218. 1615.lean
  219. 1650.lean
  220. 1650.lean.out.expected
  221. 1668.lean
  222. 1668.lean.out.expected
  223. 1674.lean
  224. 1679.lean
  225. 1681.lean
  226. 1681.lean.out.expected
  227. 1684.lean
  228. 1684.lean.out.expected
  229. 1686.lean
  230. 1692.lean
  231. 1697.lean
  232. 1711.lean
  233. 1725.lean
  234. 1730.lean
  235. 175.lean
  236. 1763.lean
  237. 1763.lean.out.expected
  238. 1779.lean
  239. 1779.lean.out.expected
  240. 1780.lean
  241. 1785.lean
  242. 1787.lean
  243. 1804.lean
  244. 1804.lean.out.expected
  245. 1808.lean
  246. 1812.lean
  247. 1812.lean.out.ignored
  248. 1813.lean
  249. 1813.lean.out.expected
  250. 1815.lean
  251. 1815.lean.out.expected
  252. 1822.lean
  253. 1829.lean
  254. 1834.lean
  255. 1841.lean
  256. 1842.lean
  257. 1842.lean.out.expected
  258. 1848.lean
  259. 1850.lean
  260. 1851.lean
  261. 1852.lean
  262. 1856.lean
  263. 1856.lean.out.expected
  264. 1869.lean
  265. 1870.lean
  266. 1878.lean
  267. 1878.lean.out.expected
  268. 1882.lean
  269. 1883.lean
  270. 1886.lean
  271. 1891.lean
  272. 1891.lean.out.expected
  273. 1892.lean
  274. 1892.lean.out.expected
  275. 1900.lean
  276. 1901.lean
  277. 1901.lean.out.expected
  278. 1907.lean
  279. 1907orig.lean
  280. 1910.lean
  281. 1918.lean
  282. 1921.lean
  283. 1926.lean
  284. 1926.lean.out.expected
  285. 1937.lean
  286. 1951.lean
  287. 1954.lean
  288. 1963.lean
  289. 1963.lean.out.expected
  290. 1968.lean
  291. 1985.lean
  292. 1986.lean
  293. 1986.lean.out.expected
  294. 2005.lean
  295. 2005.lean.out.expected
  296. 2009.lean
  297. 2018.lean
  298. 2018.lean.out.expected
  299. 2042.lean
  300. 2044.lean
  301. 2045.lean
  302. 2045.lean.out.expected
  303. 2058.lean
  304. 2073.lean
  305. 2074.lean
  306. 2077.lean
  307. 2077.lean.out.expected
  308. 2079.lean
  309. 2079.lean.out.expected
  310. 2095.lean
  311. 2115.lean
  312. 2115.lean.out.expected
  313. 2136.lean
  314. 2136.lean.out.expected
  315. 2137.lean
  316. 2143.lean
  317. 2159.lean
  318. 2161.lean
  319. 2173.lean
  320. 2178.lean
  321. 2182.lean
  322. 2186.lean
  323. 2188.lean
  324. 2199.lean
  325. 220.lean
  326. 220.lean.out.expected
  327. 2220.lean
  328. 2226.lean
  329. 223.lean
  330. 223.lean.out.expected
  331. 2243.lean
  332. 2249.lean
  333. 2262.lean
  334. 2265.lean
  335. 2265.lean.out.expected
  336. 2282.lean
  337. 2283.lean
  338. 2283.lean.out.expected
  339. 229.lean
  340. 229.lean.out.expected
  341. 2291.lean
  342. 2291.lean.out.expected
  343. 2299.lean
  344. 2311.lean
  345. 2344.lean
  346. 236.lean
  347. 236.lean.out.expected
  348. 2361.lean
  349. 2461.lean
  350. 2500.lean
  351. 2505.lean
  352. 2505.lean.out.expected
  353. 2514.lean
  354. 2552.lean
  355. 2558.lean
  356. 2558.lean.out.expected
  357. 2575.lean
  358. 2602.lean
  359. 2611.lean
  360. 2615.lean
  361. 262.lean
  362. 2649.lean
  363. 2649.lean.out.expected
  364. 2669.lean
  365. 2669.lean.out.expected
  366. 2670.lean
  367. 2672.lean
  368. 2689.lean
  369. 269.lean
  370. 2690.lean
  371. 270.lean
  372. 2710.lean
  373. 2736.lean
  374. 2736.lean.out.expected
  375. 28.lean
  376. 280.lean
  377. 281.lean
  378. 2810.lean
  379. 282.lean
  380. 2835.lean
  381. 2843.lean
  382. 2843.lean.out.expected
  383. 2846.lean
  384. 2846.lean.out.expected
  385. 2862.lean
  386. 2899.lean
  387. 2899.lean.out.expected
  388. 29.lean
  389. 2901.lean
  390. 2905.lean
  391. 2914.lean
  392. 2916.lean
  393. 2939.lean
  394. 2942.lean
  395. 2966.lean
  396. 3022.lean
  397. 3022.lean.out.expected
  398. 303.lean
  399. 3031.lean
  400. 3045.lean
  401. 305.lean
  402. 3057.lean
  403. 3057.lean.out.expected
  404. 307.lean
  405. 307.lean.out.expected
  406. 3079.lean
  407. 3091.lean
  408. 3091.lean.out.expected
  409. 310.lean
  410. 3140.lean
  411. 3140.lean.out.expected
  412. 3146.lean
  413. 3150.lean
  414. 319.lean
  415. 3214.lean
  416. 3219.lean
  417. 3229.lean
  418. 3242.lean
  419. 3257.lean
  420. 3257.lean.out.expected
  421. 326.lean
  422. 327.lean
  423. 329.lean
  424. 3313.lean
  425. 335.lean
  426. 337.lean
  427. 337.lean.out.expected
  428. 338.lean
  429. 338.lean.out.expected
  430. 3386.lean
  431. 3395.lean
  432. 34.lean
  433. 341.lean
  434. 343.lean
  435. 345.lean
  436. 3458_1.lean
  437. 3458_2.lean
  438. 3467.lean
  439. 3497.lean
  440. 3501.lean
  441. 3519.lean
  442. 3524.lean
  443. 3524.lean.out.expected
  444. 3546.lean
  445. 3547.lean
  446. 3554.lean
  447. 3643.lean
  448. 366.lean
  449. 366.lean.out.expected
  450. 3686.lean
  451. 3705.lean
  452. 3705.lean.out.expected
  453. 3706.lean
  454. 3710.lean
  455. 3713.lean
  456. 3731.lean
  457. 3740.lean
  458. 3745.lean
  459. 3791.lean
  460. 3807.lean
  461. 3807.lean.out.ignored
  462. 382.lean
  463. 382.lean.out.expected
  464. 387.lean
  465. 3922.lean
  466. 394.lean
  467. 394.lean.out.expected
  468. 3943.lean
  469. 3943.lean.out.expected
  470. 3965.lean
  471. 3965.lean.out.expected
  472. 3965_2.lean
  473. 3965_2.lean.out.expected
  474. 3965_3.lean
  475. 3965_3.lean.out.expected
  476. 3996.lean
  477. 4051.lean
  478. 4051.lean.out.expected
  479. 4064.lean
  480. 4086.lean
  481. 4086.lean.out.expected
  482. 4089.lean
  483. 4089.lean.out.expected
  484. 4101.lean
  485. 414.lean
  486. 414.lean.out.expected
  487. 4144.lean
  488. 415.lean
  489. 415.lean.out.expected
  490. 4171.lean
  491. 4171.lean.out.expected
  492. 4203.lean
  493. 421.lean
  494. 421.lean.out.expected
  495. 4213.lean
  496. 4219.lean
  497. 4230.lean
  498. 4240.lean
  499. 4240.lean.out.expected
  500. 4251.lean
  501. 4278.lean
  502. 4290.lean
  503. 4290.lean.out.expected
  504. 4306.lean
  505. 4310.lean
  506. 4313.lean
  507. 4318.lean
  508. 4320.lean
  509. 4334.lean
  510. 4339.lean
  511. 435b.lean
  512. 436.lean
  513. 4365.lean
  514. 436_lean3.lean
  515. 4375.lean
  516. 4381.lean
  517. 439.lean
  518. 439.lean.out.expected
  519. 4390.lean
  520. 4390.lean.out.expected
  521. 4398.lean
  522. 4405.lean
  523. 4406.lean
  524. 441.lean
  525. 4413.lean
  526. 445.lean
  527. 445.lean.out.expected
  528. 4452.lean
  529. 4452.lean.out.expected
  530. 4462.lean
  531. 4462.lean.out.expected
  532. 4465.lean
  533. 447_lean3.lean
  534. 447_lean3.lean.out.expected
  535. 452.lean
  536. 4534.lean
  537. 4547.lean
  538. 4555.lean
  539. 456.lean
  540. 4561.lean
  541. 457.lean
  542. 457.lean.out.expected
  543. 4573.lean
  544. 4585.lean
  545. 4585.lean.out.expected
  546. 4591.lean
  547. 4591.lean.out.expected
  548. 4595_slowdown.lean
  549. 4595_slowdown.lean.out.expected
  550. 4595_split.lean
  551. 4595_split.lean.out.expected
  552. 461a.lean
  553. 461b.lean
  554. 462.lean
  555. 463.lean
  556. 4636.lean
  557. 4636.lean.out.expected
  558. 4644.lean
  559. 4662.lean
  560. 4670.lean
  561. 4673.lean
  562. 4673.lean.out.expected
  563. 4677.lean
  564. 4686.lean
  565. 469.lean
  566. 469.lean.out.expected
  567. 470_lean3.lean
  568. 471.lean
  569. 4716.lean
  570. 474.lean
  571. 474.lean.out.expected
  572. 474_lean3.lean
  573. 474_lean3.lean.out.expected
  574. 4751.lean
  575. 4761.lean
  576. 4761.lean.out.expected
  577. 4768.lean
  578. 4773.lean
  579. 481.lean
  580. 482.lean
  581. 4845.lean
  582. 4845.lean.out.expected
  583. 4851.lean
  584. 4861.lean
  585. 4861.lean.out.expected
  586. 4888.lean
  587. 490.lean
  588. 492.lean
  589. 4920.lean
  590. 4928.lean
  591. 492_lean3.lean
  592. 492_lean3.lean.out.expected
  593. 4947.lean
  594. 498.lean
  595. 498.lean.out.expected
  596. 4983.lean
  597. 4985.lean
  598. 500_lean3.lean
  599. 500_lean3.lean.out.expected
  600. 501.lean
  601. 501.lean.out.expected
  602. 5046.lean
  603. 5046.lean.out.expected
  604. 5064.lean
  605. 509.lean
  606. 5126.lean
  607. 5176.lean
  608. 5236.lean
  609. 529.lean
  610. 529.lean.out.expected
  611. 52_lean3.lean
  612. 5333.lean
  613. 5333.lean.out.expected
  614. 5359.lean
  615. 5359.lean.out.expected
  616. 536.lean
  617. 5388.lean
  618. 5406.lean
  619. 5407.lean
  620. 5417.lean
  621. 5424.lean
  622. 5455.lean
  623. 5455.lean.out.expected
  624. 5475.lean
  625. 5565.lean
  626. 561.lean
  627. 5634.lean
  628. 5660.lean
  629. 5664.lean
  630. 5667.lean
  631. 5668.lean
  632. 5672.lean
  633. 5674.lean
  634. 5689.lean
  635. 569.lean
  636. 5755.lean
  637. 5755.lean.out.expected
  638. 5818.lean
  639. 5993.lean
  640. 602.lean
  641. 602.lean.out.expected
  642. 604.lean
  643. 604.lean.out.expected
  644. 6043.lean
  645. 6065.lean
  646. 6065.lean.out.expected
  647. 6067.lean
  648. 6067.lean.out.expected
  649. 6086.lean
  650. 6090.lean
  651. 6117.lean
  652. 6123_cat_adjunction.lean
  653. 6123_cat_adjunction.lean.out.expected
  654. 6123_mod_cast.lean
  655. 6123_mod_cast.lean.out.expected
  656. 616.lean
  657. 6164.lean
  658. 6199.lean
  659. 620.lean
  660. 620.lean.out.expected
  661. 625.lean
  662. 625.lean.out.expected
  663. 6263.lean
  664. 6263.lean.out.expected
  665. 633.lean
  666. 6332.lean
  667. 6354.lean
  668. 6373.lean
  669. 6400.lean
  670. 644.lean
  671. 646.lean
  672. 646.lean.out.ignored
  673. 6467.lean
  674. 6467.lean.out.expected
  675. 654.lean
  676. 6601.lean
  677. 664.lean
  678. 6655.lean
  679. 6694.lean
  680. 6706.lean
  681. 6759.lean
  682. 677.lean
  683. 6789.lean
  684. 679.lean
  685. 679.lean.out.expected
  686. 6927.lean
  687. 6957.lean
  688. 696.lean
  689. 6999.lean
  690. 7073.lean
  691. 7096.lean
  692. 714.lean
  693. 714.lean.out.expected
  694. 716.lean
  695. 7170.lean
  696. 7353.lean
  697. 7405.lean
  698. 7458.lean
  699. 7475.lean
  700. 753.lean
  701. 760.lean
  702. 7612.lean
  703. 7612.lean.out.expected
  704. 7638.lean
  705. 764.lean
  706. 764.lean.out.expected
  707. 7788.lean
  708. 7811.lean
  709. 783.lean
  710. 788.lean
  711. 790.lean
  712. 7927.lean
  713. 793.lean
  714. 796.lean
  715. 7993.lean
  716. 801.lean
  717. 801.lean.out.expected
  718. 8049.lean
  719. 8067.lean
  720. 813.lean
  721. 813.lean.out.expected
  722. 815.lean
  723. 815b.lean
  724. 815b.lean.out.expected
  725. 821.lean
  726. 837.lean
  727. 847.lean
  728. 854.lean
  729. 854.lean.out.expected
  730. 860.lean
  731. 8721.lean
  732. 8743.lean
  733. 879.lean
  734. 8815.lean
  735. 8894.lean
  736. 891.lean
  737. 8938.lean
  738. 9089.lean
  739. 909.lean
  740. 9156.lean
  741. 91_lean3.lean
  742. 9312.lean
  743. 9322.lean
  744. 9322.lean.out.expected
  745. 9362.lean
  746. 9363.lean
  747. 9365.lean
  748. 9366.lean
  749. 9389.lean
  750. 944.lean
  751. 9445.lean
  752. 945.lean
  753. 946.lean
  754. 9463.lean
  755. 9474.lean
  756. 948.lean
  757. 948.lean.out.expected
  758. 951.lean
  759. 951.lean.out.expected
  760. 9541.lean
  761. 955.lean
  762. 9581.lean
  763. 9591.lean
  764. 9624.lean
  765. 968.lean
  766. 9692.lean
  767. 972.lean
  768. 973.lean
  769. 973b.lean
  770. 973b.lean.out.expected
  771. 974.lean
  772. 9806.lean
  773. 9806.lean.out.expected
  774. 983.lean
  775. 983.lean.out.expected
  776. 986.lean
  777. 988.lean
  778. 988.lean.out.expected
  779. 9893.lean
  780. 9937.lean
  781. 9963.lean
  782. 9971.lean
  783. 998.lean
  784. 998Export.lean
  785. abst.lean
  786. abst.lean.out.expected
  787. abstractExpr.lean
  788. abstractMVars.lean
  789. ac_expr.lean
  790. ac_expr.lean.out.expected
  791. ac_rfl.lean
  792. ac_rfl.lean.out.expected
  793. ack.lean
  794. acLt_timeout.lean
  795. ACltBug.lean
  796. adam1.lean
  797. adam1.lean.out.expected
  798. adamTC.lean
  799. adamTC2.lean
  800. add_suggestion.lean
  801. addDecorationsWithoutPartial.lean
  802. addPPExplicitToExposeDiff.lean
  803. aesop_run_metam.lean
  804. aig_optimizations.lean
  805. aig_stress.lean
  806. alex1.lean
  807. alex1.lean.out.expected
  808. alg.lean
  809. alias.lean
  810. allFieldForConstants.lean
  811. allFieldForConstants.lean.out.expected
  812. allGoals.lean
  813. and_intros.lean
  814. andCasesOnBug.lean
  815. anonBinderName.lean
  816. anonymous_ctor_error_msg.lean
  817. anonymousCtor.lean
  818. appFinalizeIssue.lean
  819. appFinalizeIssue.lean.out.expected
  820. appIssue.lean
  821. apply_error.lean
  822. apply_subgoal_name_issue.lean
  823. apply_tac.lean
  824. applytransp.lean
  825. appParserIssue.lean
  826. appParserIssue.lean.out.expected
  827. approxDepth.lean
  828. approxDepth.lean.out.expected
  829. array1.lean
  830. array1.lean.out.expected
  831. array_isEqvAux.lean
  832. array_simp.lean
  833. arrayDecEq.lean
  834. arrayGetU.lean
  835. arrayGetU.lean.out.expected
  836. arrowDot.lean
  837. arthur1.lean
  838. arthur2.lean
  839. arthur2.lean.out.expected
  840. as_aux_lemma.lean
  841. assertAfterBug.lean
  842. assertAfterBug.lean.out.expected
  843. assertExists.lean
  844. aStructPerfIssue.lean
  845. async.lean
  846. async.lean.out.expected
  847. async_base_functions.lean
  848. async_cancellation.lean
  849. async_cancellation.lean.serial
  850. async_cancellation_reasons.lean
  851. async_dns.lean
  852. async_dns.lean.serial
  853. async_http_body.lean
  854. async_http_body_framing.lean
  855. async_http_dispatch.lean
  856. async_http_encode.lean
  857. async_http_expect.lean
  858. async_http_fuzz.lean
  859. async_http_fuzz.lean.serial
  860. async_http_fuzz_limits.lean
  861. async_http_fuzz_limits.lean.serial
  862. async_http_fuzz_random.lean
  863. async_http_fuzz_random.lean.serial
  864. async_http_h1_incremental.lean
  865. async_http_h1_parser_fuzz.lean
  866. async_http_h1_rfc_compliance.lean
  867. async_http_hang_regressions.lean
  868. async_http_hang_regressions.lean.serial
  869. async_http_headers.lean
  870. async_http_keepalive.lean
  871. async_http_request_headers.lean
  872. async_http_request_line.lean
  873. async_http_response_framing.lean
  874. async_http_string_quoting.lean
  875. async_http_trailers.lean
  876. async_http_uri.lean
  877. async_select_channel.lean
  878. async_select_combine.lean
  879. async_select_gate.lean
  880. async_select_socket.lean
  881. async_select_socket.lean.out.expected
  882. async_select_socket.lean.serial
  883. async_select_timer.lean
  884. async_select_timer.lean.serial
  885. async_streammap.lean
  886. async_surface_sleep.lean
  887. async_systems_info.lean
  888. async_systems_info.lean.out.ignored
  889. async_tcp_fname_errors.lean
  890. async_tcp_half.lean
  891. async_tcp_server_client.lean
  892. async_udp_sockets.lean
  893. atomValidation.lean
  894. attachJp.lean
  895. attachJp.lean.out.expected
  896. attributeErrors.lean
  897. autoboundIssues.lean
  898. autoboundIssues.lean.out.expected
  899. autoImplicitChain.lean
  900. autoImplicitChain.lean.out.expected
  901. autoLift.lean
  902. autoLiftIssue.lean
  903. autoparam.lean
  904. autoparam.lean.out.expected
  905. auxinvariable.lean
  906. auxParentProj.lean
  907. auxParentProj.lean.out.expected
  908. backtrackable_estate.lean
  909. balg.lean
  910. baseIO.lean
  911. baseIO.lean.out.expected
  912. betaSimp.lean
  913. bhaviksSampler.lean
  914. bhaviksSampler.lean.out.expected
  915. bigctor.lean
  916. bigFromJson.lean
  917. bigmul.lean
  918. bigop.lean
  919. bigop.lean.out.expected
  920. bindCasesIssue.lean
  921. bindCasesIssue.lean.out.ignored
  922. binder_predicates.lean
  923. binder_predicates.lean.out.expected
  924. binderCacheIssue.lean
  925. binderCacheIssue.lean.out.expected
  926. binderCacheIssue2.lean
  927. binderCacheIssue2.lean.out.expected
  928. binderNameHint.lean
  929. binderNameHint_congr.lean
  930. binderNameHintScope.lean
  931. binderNameHintSimp.lean
  932. binderNotation.lean
  933. binderNotation.lean.out.expected
  934. bindersAbstractingUnassignedMVars.lean
  935. bindersAbstractingUnassignedMVars.lean.out.expected
  936. binop.lean
  937. binop_binrel_perf_issue.lean
  938. binop_binrel_perf_issue.lean.out.expected
  939. binop_lazy.lean
  940. binop_lazy.lean.out.expected
  941. binopInfoTree.lean
  942. binopInfoTree.lean.out.expected
  943. binrec.lean
  944. binrec.lean.out.ignored
  945. binrel.lean
  946. binrel_binop.lean
  947. binrel_binop.lean.out.expected
  948. binrelmacros.lean
  949. binrelmacros.lean.out.expected
  950. binsearch.lean
  951. binsearch.lean.out.expected
  952. bintreeGoal.lean
  953. bintreeGoal.lean.out.expected
  954. bitvec.lean
  955. bitvec_fin_literal_norm.lean
  956. bitvec_fin_literal_norm.lean.out.expected
  957. bitvec_simproc.lean
  958. bitwise.lean
  959. bitwise.lean.out.expected
  960. bool2int.lean
  961. bool2int.lean.out.expected
  962. bool_simp.lean
  963. borrowBug.lean
  964. boxing_bug.lean
  965. broadcast.lean
  966. bubble.lean
  967. bugNatLitDiscrTree.lean
  968. builtinInitStx.lean
  969. builtinSimprocTrace.lean
  970. builtinSimprocTrace.lean.out.expected
  971. bv_arith.lean
  972. bv_axiom_check.lean
  973. bv_bitblast_stress.lean
  974. bv_bitwise.lean
  975. bv_cast.lean
  976. bv_counterexample.lean
  977. bv_decide_bool.lean
  978. bv_decide_enum_dependent.lean
  979. bv_decide_enum_universe.lean
  980. bv_decide_enums_two.lean
  981. bv_decide_nat.lean
  982. bv_decide_rewriter.lean
  983. bv_decide_rewriter.lean.out.expected
  984. bv_decide_rewriter_ac_nf.lean
  985. bv_decide_shift_error.lean
  986. bv_decide_shift_to_nat.lean
  987. bv_decide_solver_modes.lean
  988. bv_enums.lean
  989. bv_errors.lean
  990. bv_extract.lean
  991. bv_inequality.lean
  992. bv_llvm.lean
  993. bv_math_lit_perf.lean
  994. bv_math_lit_perf.lean.out.expected
  995. bv_parametric_struct.lean
  996. bv_popcount.lean
  997. bv_preprocess_stress.lean
  998. bv_reflection_stress.lean
  999. bv_relation.lean
  1000. bv_shift.lean
  1001. bv_sint.lean
  1002. bv_structures.lean
  1003. bv_substructure.lean
  1004. bv_uint.lean
  1005. bv_uninterpreted.lean
  1006. bv_unused.lean
  1007. bv_will_overflow.lean
  1008. bvarcrash.lean
  1009. by_cases.lean
  1010. byAsSorry.lean
  1011. byCasesMetaM.lean
  1012. byCasesMetaM.lean.out.expected
  1013. bytearray.lean
  1014. bytearray.lean.out.expected
  1015. bytearray_eq.lean
  1016. byteslice.lean
  1017. byteSliceIssue.lean
  1018. byteSliceIssue.lean.out.expected
  1019. cacheIssue.lean
  1020. cacheIssue.lean.out.expected
  1021. calc.lean
  1022. calc.lean.out.expected
  1023. calcBug.lean
  1024. calcInType.lean
  1025. cancel_token.lean
  1026. cancellation_context.lean
  1027. canonM_exists_fun.lean
  1028. casePrime.lean
  1029. casesAnyTypeIssue.lean
  1030. casesOnAcc.lean
  1031. casesOnCases.lean
  1032. casesOnSameCtor.lean
  1033. casesRec.lean
  1034. casesTactic.lean
  1035. casesUsing.lean
  1036. casesUsing.lean.out.expected
  1037. caseTacInMacros.lean
  1038. catchThe.lean
  1039. cbv1.lean
  1040. cbv2.lean
  1041. cbv3.lean
  1042. cbv4.lean
  1043. cbv_annotations2.lean
  1044. cbv_annotations3.lean
  1045. cbv_annotations4.lean
  1046. cbv_annotations5.lean
  1047. cbv_annotations6.lean
  1048. cbv_array.lean
  1049. cbv_at.lean
  1050. cbv_brackets.lean
  1051. cbv_classical.lean
  1052. cbv_decidable_congr.lean
  1053. cbv_decide_simproc.lean
  1054. cbv_dep_proj.lean
  1055. cbv_eval_erase.lean
  1056. cbv_eval_inv.lean
  1057. cbv_hashmap_annotations.lean
  1058. cbv_ite_issue.lean
  1059. cbv_iter.lean
  1060. cbv_max_steps.lean
  1061. cbv_nullary.lean
  1062. cbv_opaque_guard.lean
  1063. cbv_opaque_inline.lean
  1064. cbv_opaque_reducible.lean
  1065. cbv_proj_arg_bug.lean
  1066. cbv_simproc.lean
  1067. cbv_simproc_errors.lean
  1068. cbv_simproc_fib.lean
  1069. cbv_string.lean
  1070. cbv_string_split.lean
  1071. cceScoping.lean
  1072. cdotAtSimpArg.lean
  1073. cdotTests.lean
  1074. cdotTuple.lean
  1075. cdotTuple.lean.out.expected
  1076. change.lean
  1077. charQuote.lean
  1078. charrange.lean
  1079. check.lean
  1080. check_failure.lean
  1081. check_failure.lean.out.expected
  1082. checkAssignmentIssue.lean
  1083. choiceExpectedTypeBug.lean
  1084. choiceExpectedTypeBug.lean.out.expected
  1085. choiceMacroRules.lean
  1086. choiceMacroRules.lean.out.expected
  1087. class_inductive.lean
  1088. class_inductive.lean.out.expected
  1089. classAbbrev.lean
  1090. classDefReducibilityAfterAttr.lean
  1091. classical.lean
  1092. cleanup_forallTelescope.lean
  1093. cleanupTypeAnnotations.lean
  1094. clear_value.lean
  1095. closure1.lean
  1096. codeBindUnreachIssue.lean
  1097. codeBindUnreachIssue.lean.out.ignored
  1098. coe.lean
  1099. coe.lean.out.expected
  1100. coeAttr1.lean
  1101. coeAttr1.lean.out.expected
  1102. coeAttrs.lean
  1103. coeIssue1.lean
  1104. coeIssue1.lean.out.expected
  1105. coeIssue2.lean
  1106. coeIssue2.lean.out.expected
  1107. coeIssue3.lean
  1108. coeIssue3.lean.out.expected
  1109. coeIssues4.lean
  1110. coelambda.lean
  1111. coeM.lean
  1112. coeM.lean.out.expected
  1113. CoeNew.lean
  1114. CoeNew.lean.out.expected
  1115. coeOutParamIssue.lean
  1116. coeOutParamIssue2.lean
  1117. coeOutParamIssue2.lean.out.expected
  1118. coeSort1.lean
  1119. coeSort2.lean
  1120. coeSort2.lean.out.expected
  1121. coinductive_instance.lean
  1122. coinductive_instance.lean.out.expected
  1123. coinductive_predicates.lean
  1124. coinductive_predicates_errors.lean
  1125. coinductive_syntax.lean
  1126. collectAxioms.lean
  1127. collectLooseBVars.lean
  1128. combinatorsAndWF.lean
  1129. CommandExtOverlap.lean
  1130. compatibleTypesEtaIssue.lean
  1131. compatibleTypesEtaIssue.lean.out.expected
  1132. compile_bool_const_fold_bug.lean
  1133. compile_borrowed_reset_jp.lean
  1134. compile_coalesce_rc.lean
  1135. compile_drop_specialization.lean
  1136. compile_multi_panic.lean
  1137. compile_recursive_array_access.lean
  1138. compiler_bug_neutral.lean
  1139. compiler_disable_borrow_annotations.lean
  1140. compiler_erase_bug.lean
  1141. compiler_fold_usize.lean
  1142. compiler_proj_bug.lean
  1143. compiler_push_proj.lean
  1144. compiler_type_transparency.lean
  1145. computedFields.lean
  1146. computedFieldsCode.lean
  1147. computedFieldsCode.lean.out.expected
  1148. concatElim.lean
  1149. config_eval.lean
  1150. congrReserved.lean
  1151. congrSimpBug.lean
  1152. congrSimpDeclKinds.lean
  1153. congrSimpMathlibIssue.lean
  1154. congrTactic.lean
  1155. congrThm.lean
  1156. congrThm.lean.out.expected
  1157. congrThm2.lean
  1158. congrThm3.lean
  1159. congrThmIssue.lean
  1160. congrThmIssue.lean.out.expected
  1161. const_fold_reprFast.lean
  1162. constant_fold_task_get_pure.lean
  1163. constantCompilerBug.lean
  1164. constantCompilerBug.lean.out.expected
  1165. constDelab.lean
  1166. constDelab.lean.out.expected
  1167. constFun.lean
  1168. constFun2.lean
  1169. constProp.lean
  1170. constProp.lean.out.expected
  1171. constructor_as_variable.lean
  1172. consumePPHint.lean
  1173. consumePPHint.lean.out.expected
  1174. context_async.lean
  1175. contra.lean
  1176. contradiction1.lean
  1177. contradictionExfalso.lean
  1178. contradictionLoop.lean
  1179. conv1.lean
  1180. conv2.lean
  1181. conv_arg.lean
  1182. convcalc.lean
  1183. convClear.lean
  1184. convInConv.lean
  1185. convInConv.lean.out.expected
  1186. convPatternAtLetIssue.lean
  1187. convPatternAtLetIssue.lean.out.expected
  1188. convPatternMatchIssue.lean
  1189. convPatternMatchIssue.lean.out.expected
  1190. convZetaLetExt.lean
  1191. convZetaLetExt.lean.out.expected
  1192. core.lean
  1193. crashDiv0.lean
  1194. crlfToLf.lean
  1195. csimp_type_error.lean
  1196. csimpAttrAppend.lean
  1197. csimpAttrAppend.lean.out.expected
  1198. csimpAttrFn.lean
  1199. csimpCore.lean
  1200. ctor_layout.lean
  1201. ctor_layout.lean.out.expected
  1202. ctorAutoParams.lean
  1203. ctorAutoParams.lean.out.expected
  1204. ctorElim.lean
  1205. ctorFieldVisibilityHints.lean
  1206. ctorIdx.lean
  1207. ctorIdxHInj.lean
  1208. ctorMixedRelevance.lean
  1209. currentDir.lean
  1210. currentDir.lean.out.ignored
  1211. customEliminators.lean
  1212. cutsat_lia_deprecation.lean
  1213. Daniel1.lean
  1214. dateTimeOrd.lean
  1215. dbgMacros.lean
  1216. dbgMacros.lean.init.sh
  1217. dbgMacros.lean.out.expected
  1218. deBruijn.lean
  1219. decAuxBug.lean
  1220. decClassical.lean
  1221. decEq.lean
  1222. decEqMutualInductives.lean
  1223. decEqMutualInductives.lean.out.expected
  1224. decEqNonInjIndex.lean
  1225. decidability_timeout.lean
  1226. Decidable-decide-erasure.lean
  1227. decidableBallLT_tailRecursive.lean
  1228. decide_cbv1.lean
  1229. decide_cbv_errors.lean
  1230. decidelet.lean
  1231. decideNative.lean
  1232. decideNative.lean.out.expected
  1233. decideNativePanic.lean
  1234. decideNativePanic.lean.init.sh
  1235. decideNativePanic.lean.out.expected
  1236. decideTactic.lean
  1237. decideTacticKernel.lean
  1238. decimals.lean
  1239. decimals.lean.out.expected
  1240. declareConfigElabBug.lean
  1241. declareConfigElabIssue.lean
  1242. decreasingTacticUpdatedEnvIssue.lean
  1243. deep1.lean
  1244. def1.lean
  1245. def10.lean
  1246. def11.lean
  1247. def12.lean
  1248. def13.lean
  1249. def14.lean
  1250. def15.lean
  1251. def16.lean
  1252. def17.lean
  1253. def18.lean
  1254. def19.lean
  1255. def2.lean
  1256. def20.lean
  1257. def3.lean
  1258. def4.lean
  1259. def5.lean
  1260. def6.lean
  1261. def6.lean.out.expected
  1262. def7.lean
  1263. def8.lean
  1264. def9.lean
  1265. defaultEliminator.lean
  1266. defaultInstanceWithPrio.lean
  1267. defaultInstanceWithPrio.lean.out.expected
  1268. defaultInstBacktrackIssue.lean
  1269. defaultInstBacktrackIssue.lean.out.expected
  1270. defaultValueParamIssue.lean
  1271. DefEqAssignBug.lean
  1272. defeqAttrib.lean
  1273. defeqAttribStrictOnly.lean
  1274. defEqVsWhnfI.lean
  1275. delabApp.lean
  1276. delabConst.lean
  1277. delabDoLetFun.lean
  1278. delabDoLetFun.lean.out.expected
  1279. delabMatch.lean
  1280. delabName.lean
  1281. delabOverApp.lean
  1282. delabOverApp.lean.out.expected
  1283. delabProjectionApp.lean
  1284. delabStdRange.lean
  1285. delabStructInst.lean
  1286. delabUnexpand.lean
  1287. delabUnexpand.lean.out.expected
  1288. deltaRedIndPredBelow.lean
  1289. demangling.lean
  1290. depElim1.lean
  1291. depElim1.lean.out.expected
  1292. depFieldIssue.lean
  1293. depFieldIssue.lean.out.ignored
  1294. depHd.lean
  1295. deprecated_arg.lean
  1296. deprecated_module.lean
  1297. deprecated_syntax.lean
  1298. deprecated_syntax.lean.out.expected
  1299. deprecated_warning.lean
  1300. deprecatedModule.lean
  1301. deprecatedOptions.lean
  1302. deq.lean
  1303. deriv.lean
  1304. deriving_diamond_defeq.lean
  1305. derivingBEq.lean
  1306. derivingBEqLinear.lean
  1307. derivingDecidableEq.lean
  1308. derivingDecidableEq.lean.out.expected
  1309. derivingDecidableEq2.lean
  1310. derivingDecidableEqLinear.lean
  1311. derivingDelta.lean
  1312. derivingHashable.lean
  1313. derivingHashable.lean.out.expected
  1314. derivingHashable2.lean
  1315. derivingInhabited.lean
  1316. derivingNonempty.lean
  1317. derivingReflBEq.lean
  1318. derivingRepr.lean
  1319. derivingRpcEncoding.lean
  1320. derivingRpcEncoding.lean.out.expected
  1321. derivingToExpr.lean
  1322. diagnostics.lean
  1323. diagnosticsMsgOptional.lean
  1324. diagRec.lean
  1325. diamond1.lean
  1326. diamond10.lean
  1327. diamond10.lean.out.expected
  1328. diamond11.lean
  1329. diamond12.lean
  1330. diamond13.lean
  1331. diamond2.lean
  1332. diamond2.lean.out.expected
  1333. diamond3.lean
  1334. diamond3.lean.out.expected
  1335. diamond4.lean
  1336. diamond4.lean.out.expected
  1337. diamond5.lean
  1338. diamond6.lean
  1339. diamond6.lean.out.expected
  1340. diamond7.lean
  1341. diamond7.lean.out.expected
  1342. diamond8.lean
  1343. diamond8.lean.out.expected
  1344. diamond9.lean
  1345. diamond9.lean.out.expected
  1346. diff.lean
  1347. discrRefinement.lean
  1348. discrRefinement2.lean
  1349. discrRefinement3.lean
  1350. discrTreeIota.lean
  1351. discrTreeIota.lean.out.expected
  1352. discrTreeKey.lean
  1353. discrTreeKey.lean.out.expected
  1354. discrTreeOffset.lean
  1355. discrTreeSimp.lean
  1356. discrTreeSimp.lean.out.expected
  1357. divExact.lean
  1358. do_eqv.lean
  1359. do_eqv_proofs.lean
  1360. do_for_loop_compiler_test.lean
  1361. do_for_loop_levenstein_compiler_test.lean
  1362. doControlInfoAggregate.lean
  1363. docstringRewrites.lean
  1364. doDepIfAnon.lean
  1365. doElemAsTermNotation.lean
  1366. doElemControlInfoAttribute.lean
  1367. doForInvariant.lean
  1368. doForMutSortPoly.lean
  1369. doForMutUniv.lean
  1370. doForward.lean
  1371. dofun_prec.lean
  1372. doIfLet.lean
  1373. doIfLet.lean.out.expected
  1374. doLetArrowPatExpectedType.lean
  1375. doLetConfig.lean
  1376. doLetElse.lean
  1377. doLetElseIndent.lean
  1378. dollarProjIssue.lean
  1379. doLogicTests.lean
  1380. doMatchDependent.lean
  1381. doMatchDiscrDep.lean
  1382. doNotation1.lean
  1383. doNotation2.lean
  1384. doNotation3.lean
  1385. doNotation4.lean
  1386. doNotation5.lean
  1387. doNotation6.lean
  1388. doNotation6.lean.out.expected
  1389. doNotation7.lean
  1390. doNotationIndexedMonad.lean
  1391. doNotationPluggableOps.lean
  1392. Dorais1.lean
  1393. Dorais1.lean.out.expected
  1394. doSyntaxPatternError.lean
  1395. dotNameIssue.lean
  1396. dotNotationAndDefaultInstance.lean
  1397. dotNotationRecDecl.lean
  1398. doTrailingAtEOI.lean
  1399. doTryCatchCoerce.lean
  1400. dottedCtorNamedArgPattern.lean
  1401. dottedIdentNotation.lean
  1402. dottedNameBug.lean
  1403. double_match.lean
  1404. doubleReset.lean
  1405. doubleReset.lean.out.expected
  1406. dsimp1.lean
  1407. dsimp2.lean
  1408. dsimp_bv_simproc.lean
  1409. dsimp_instances.lean
  1410. dsimp_proofs.lean
  1411. dsimpBackwardDefEqTrace.lean
  1412. dsimpNatLitIssue.lean
  1413. dsimproc.lean
  1414. dsimpZetaIssue.lean
  1415. dsimpZetaIssue.lean.out.expected
  1416. due_to_metavariables.lean
  1417. duplicatedArgumentApplicationTypeMismatch.lean
  1418. dvd_simproc.lean
  1419. DVec.lean
  1420. DVec.lean.out.expected
  1421. dynamic.lean
  1422. eagerCoeExpansion.lean
  1423. eagerCoeExpansion.lean.out.expected
  1424. eagerInliningIssue.lean
  1425. elab_cmd.lean
  1426. elab_cmd.lean.out.expected
  1427. elabAsElim.lean
  1428. elabAsElim.lean.out.expected
  1429. elabCmd.lean
  1430. elabIte.lean
  1431. elabLet.lean
  1432. elabToSyntax.lean
  1433. elim_dead_vars.lean
  1434. elimDeadBranchesCtorParams.lean
  1435. elimDeadBranchesUInt64Literal.lean
  1436. elimDeadBranchesUInt64Literal.lean.out.expected
  1437. eliminatorImplicitTargets.lean
  1438. elimOptParam.lean
  1439. elseCaseArrow.lean
  1440. elseIfConfusion.lean
  1441. emptycOverloadIssues.lean
  1442. emptyEnvVar.lean
  1443. emptyLcnf.lean
  1444. endErrors.lean
  1445. enumDecEq.lean
  1446. enumNoConfusionIssue.lean
  1447. enumsModuloIrrelevance.lean
  1448. env_linter.lean
  1449. eq_some_iff_get_eq_issue.lean
  1450. eqndrecEtaLCNFIssue.lean
  1451. eqndrecEtaLCNFIssue.lean.out.expected
  1452. eqnOptions.lean
  1453. eqnsAtSimp.lean
  1454. eqnsAtSimp.lean.out.expected
  1455. eqnsAtSimp2.lean
  1456. eqnsAtSimp3.lean
  1457. eqnsAtSimp3.lean.out.expected
  1458. eqnsPrio.lean
  1459. eqnsProjections.lean
  1460. eqnsReducible.lean
  1461. eqRecursors.lean
  1462. eqTheoremForVec.lean
  1463. eqThm.lean
  1464. eqThm.lean.out.expected
  1465. eqThmWithMoreThanOneAsPattern.lean
  1466. eqValue.lean
  1467. erased.lean
  1468. eraseReps.lean
  1469. eraseSimp.lean
  1470. eraseSimp.lean.out.expected
  1471. eraseSuffix.lean
  1472. erasureConfusion.lean
  1473. errorExplanationElab.lean
  1474. errorExplanationLinting.lean
  1475. eta.lean
  1476. eta.lean.out.expected
  1477. eta_lambda_lift.lean
  1478. etaFirst.lean
  1479. etaReducedMvarAssignments.lean
  1480. etaReducedMvarAssignments.lean.out.expected
  1481. etaStruct.lean
  1482. etaStruct.lean.out.expected
  1483. etaStructProofIrrelIssue.lean
  1484. eval.lean
  1485. eval_unboxed_const.lean
  1486. evalBuiltinInit.lean
  1487. evalCmd.lean
  1488. evalCmd.lean.out.expected
  1489. evalconst.lean
  1490. evalDo.lean
  1491. evalInit.lean
  1492. evalInit.lean.out.ignored
  1493. evalProp.lean
  1494. evalTacticBug.lean
  1495. exact_private.lean
  1496. exact_rw_deprecated.lean
  1497. exfalsoBug.lean
  1498. exists.lean
  1499. exp.lean
  1500. expandAbbrevAtIsClass.lean
  1501. expandExplicitBinders.lean
  1502. expandExplicitBinders.lean.out.expected
  1503. expandWhereStructInstIssue.lean
  1504. expectedTypePropagation.lean
  1505. explicitApp.lean
  1506. explicitApp.lean.out.expected
  1507. explicitMotive.lean
  1508. explicitOpenDeclIssue.lean
  1509. explicitOpenDeclIssue.lean.out.expected
  1510. exposeArrayBack.lean
  1511. exposeDiff.lean
  1512. exposeNames.lean
  1513. exposeNames.lean.out.expected
  1514. expr1.lean
  1515. expr_maps.lean
  1516. ExprLens.lean
  1517. ext.lean
  1518. ext1.lean
  1519. ext1.lean.out.expected
  1520. extensibleTacticBug.lean
  1521. extern.lean
  1522. externBoxing.lean
  1523. externBoxing.lean.out.expected
  1524. exthashset_deceq.lean
  1525. extmacro.lean
  1526. extract.lean
  1527. extract.lean.out.expected
  1528. extract_array_lit.lean
  1529. extract_lets.lean
  1530. extractClosed.lean
  1531. extraModUses.lean
  1532. exttreeset_deceq.lean
  1533. exttreeset_deceq.lean.out.expected
  1534. false_or_by_contra.lean
  1535. falseElimAtSimpLocalDecl.lean
  1536. fib_correct.lean
  1537. fieldAbbrevInPat.lean
  1538. fieldAutoBound.lean
  1539. fieldDefaultValueWithoutType.lean
  1540. fieldIssue.lean
  1541. fieldNamesWithMinus.lean
  1542. fieldTypeBug.lean
  1543. fieldTypeBug.lean.out.ignored
  1544. filePath.lean
  1545. filePath.lean.out.expected
  1546. filter.lean
  1547. fin_coercions.lean
  1548. fin_two_pow.lean
  1549. finally.lean
  1550. finDotCtor.lean
  1551. findPrivateDocString.lean
  1552. finLit.lean
  1553. finMatch.lean
  1554. fixedIndexToParamIssue.lean
  1555. fixedIndexToParamIssue.lean.out.expected
  1556. fixedIndicesToParams.lean
  1557. fixedIndicesToParams.lean.out.expected
  1558. fixedParams.lean
  1559. fixedParamsAnnot.lean
  1560. fixedParamsDep.lean
  1561. fixedParamsReorder.lean
  1562. fixedParamsStructDeps.lean
  1563. flat_expr.lean
  1564. float1.lean
  1565. float32.lean
  1566. float_cases_bug.lean
  1567. float_compiler.lean
  1568. float_conversions.lean
  1569. float_from_bignum.lean
  1570. float_model_tobits.lean
  1571. floatarray.lean
  1572. floatBits.lean
  1573. floatEquality.lean
  1574. floatLetIn.lean
  1575. floatModelDefeq.lean
  1576. floatOptParam.lean
  1577. foApprox.lean
  1578. fold_uint.lean
  1579. foldConsts.lean
  1580. foldLits.lean
  1581. foldLits.lean.out.expected
  1582. foldlUnsafe_bug.lean
  1583. foldProjs.lean
  1584. foldProjs.lean.out.expected
  1585. forallMetaBounded.lean
  1586. forallMetaBounded.lean.out.expected
  1587. forBodyResultTypeIssue.lean
  1588. forIn_phashset.lean
  1589. forInColErr.lean
  1590. forInElabBug.lean
  1591. forInListSpecUnivPoly.lean
  1592. forInListSpecUnivPoly.lean.out.expected
  1593. forInPArray.lean
  1594. forInRangeWF.lean
  1595. forInReturnPropagation.lean
  1596. forInUniv.lean
  1597. Format.lean
  1598. Format.lean.out.expected
  1599. formatHardLineBreaks.lean
  1600. formatTerm.lean
  1601. formatTerm.lean.out.expected
  1602. formatterTokenTable.lean
  1603. forOutParamIssue.lean
  1604. forOutParamIssue.lean.out.expected
  1605. forParallel.lean
  1606. french_ident.lean
  1607. french_quote.lean
  1608. frontend_meeting_2022_09_13.lean
  1609. frontend_meeting_2022_09_13.lean.out.expected
  1610. fun.lean
  1611. fun.lean.out.expected
  1612. fun_cases.lean
  1613. funext.lean
  1614. funind_demo.lean
  1615. funind_expr.lean
  1616. funind_fewer_levels.lean
  1617. funind_mutual_dep.lean
  1618. funind_proof.lean
  1619. funind_structural.lean
  1620. funind_structural_mutual.lean
  1621. funind_tests.lean
  1622. funind_unfolding.lean
  1623. funInduction.lean
  1624. funinduction_generalize.lean
  1625. funinduction_ident.lean
  1626. funInfoBug.lean
  1627. funInfoBug.lean.out.expected
  1628. funMatchIssue.lean
  1629. fvarSubset.lean
  1630. gcd.lean
  1631. gcd.lean.out.expected
  1632. generalize.lean
  1633. generalizeMany.lean
  1634. generalizeTelescope.lean
  1635. genindices.lean
  1636. getArgPrime.lean
  1637. getElemV.lean
  1638. getline_crash.lean
  1639. getline_crash.lean.before.sh
  1640. globalAttributesIn.lean
  1641. grandparentImplicitReducible.lean
  1642. grind_10160.lean
  1643. grind_10160.lean.out.expected
  1644. grind_10232.lean
  1645. grind_10232.lean.out.expected
  1646. grind_10233.lean
  1647. grind_10233.lean.out.expected
  1648. grind_10317.lean
  1649. grind_10489.lean
  1650. grind_10500.lean
  1651. grind_10622.lean
  1652. grind_10622.lean.out.expected
  1653. grind_10661.lean
  1654. grind_10670.lean
  1655. grind_10885.lean
  1656. grind_10953.lean
  1657. grind_10983.lean
  1658. grind_11001.lean
  1659. grind_11001.lean.out.expected
  1660. grind_11036.lean
  1661. grind_11081.lean
  1662. grind_11081.lean.out.expected
  1663. grind_11086.lean
  1664. grind_11086.lean.out.expected
  1665. grind_11088.lean
  1666. grind_11124.lean
  1667. grind_11124.lean.out.expected
  1668. grind_11130.lean
  1669. grind_11130.lean.out.expected
  1670. grind_11134.lean
  1671. grind_11134.lean.out.expected
  1672. grind_11259.lean
  1673. grind_11449.lean
  1674. grind_11477.lean
  1675. grind_11498.lean
  1676. grind_11498.lean.out.expected
  1677. grind_11515.lean
  1678. grind_11539.lean
  1679. grind_11539_2.lean
  1680. grind_11545.lean
  1681. grind_11545.lean.out.expected
  1682. grind_11597.lean
  1683. grind_11597.lean.out.expected
  1684. grind_11622.lean
  1685. grind_11633.lean
  1686. grind_11690.lean
  1687. grind_11690.lean.out.expected
  1688. grind_11697_a.lean
  1689. grind_11697_b.lean
  1690. grind_11738.lean
  1691. grind_11745.lean
  1692. grind_11745_extra.lean
  1693. grind_11930.lean
  1694. grind_12140.lean
  1695. grind_12246.lean
  1696. grind_12246.lean.out.expected
  1697. grind_12390.lean
  1698. grind_12428.lean
  1699. grind_12428.lean.out.expected
  1700. grind_12581.lean
  1701. grind_12812.lean
  1702. grind_13167.lean
  1703. grind_13573.lean
  1704. grind_13773.lean
  1705. grind_13877.lean
  1706. grind_13877.lean.out.expected
  1707. grind_9216.lean
  1708. grind_9321.lean
  1709. grind_9427.lean
  1710. grind_9467.lean
  1711. grind_9477.lean
  1712. grind_9485.lean
  1713. grind_9485.lean.out.expected
  1714. grind_9562.lean
  1715. grind_9572.lean
  1716. grind_9610.lean
  1717. grind_9769.lean
  1718. grind_9825.lean
  1719. grind_9828.lean
  1720. grind_9830.lean
  1721. grind_9854.lean
  1722. grind_9856.lean
  1723. grind_9856.lean.out.expected
  1724. grind_9897.lean
  1725. grind_9899.lean
  1726. grind_9907.lean
  1727. grind_9948.lean
  1728. grind_abstract_mvars.lean
  1729. grind_ac_1.lean
  1730. grind_ac_2.lean
  1731. grind_ac_3.lean
  1732. grind_ac_4.lean
  1733. grind_ac_5.lean
  1734. grind_ac_inv_issue.lean
  1735. grind_ac_inv_issue_2.lean
  1736. grind_activate_local_issue.lean
  1737. grind_all_singleton_patterns.lean
  1738. grind_alphaShare_builder.lean
  1739. grind_annotated.lean
  1740. grind_append_issue.lean
  1741. grind_append_issue.lean.out.expected
  1742. grind_arbitrary_params.lean
  1743. grind_arith_nonstd_insts.lean
  1744. grind_array.lean
  1745. grind_array_attach.lean
  1746. grind_assoc.lean
  1747. grind_assoc.lean.out.expected
  1748. grind_attrs.lean
  1749. grind_attrs.lean.out.expected
  1750. grind_beta.lean
  1751. grind_beta_generation_check.lean
  1752. grind_big_poly.lean
  1753. grind_bigstep.lean
  1754. grind_bintree.lean
  1755. grind_bintree.lean.out.expected
  1756. grind_bitvec.lean
  1757. grind_bool_diseq.lean
  1758. grind_bool_prop.lean
  1759. grind_canon_bug.lean
  1760. grind_canon_bug.lean.out.expected
  1761. grind_canon_bug_2.lean
  1762. grind_canon_insts.lean
  1763. grind_canon_insts.lean.out.expected
  1764. grind_canon_ofnat.lean
  1765. grind_canon_ofnat.lean.out.expected
  1766. grind_canon_types.lean
  1767. grind_canon_types.lean.out.expected
  1768. grind_cases.lean
  1769. grind_cases_anchor_ordinal.lean
  1770. grind_cases_tac.lean
  1771. grind_cases_tac.lean.out.expected
  1772. grind_casting_issue.lean
  1773. grind_cat.lean
  1774. grind_cat2.lean
  1775. grind_cat2.lean.out.expected
  1776. grind_clean_den.lean
  1777. grind_clear_error.lean
  1778. grind_clear_error.lean.out.expected
  1779. grind_commsemiring.lean
  1780. grind_congr.lean
  1781. grind_congr.lean.out.expected
  1782. grind_congr1.lean
  1783. grind_congr1.lean.out.expected
  1784. grind_congr_hash_issue.lean
  1785. grind_congr_over_applied.lean
  1786. grind_const_pattern.lean
  1787. grind_const_pattern.lean.out.expected
  1788. grind_constProp.lean
  1789. grind_constProp.lean.out.expected
  1790. grind_countP.lean
  1791. grind_ctor_ematch.lean
  1792. grind_ctor_ematch.lean.out.expected
  1793. grind_ctorIdx.lean
  1794. grind_cutsat_auto.lean
  1795. grind_cutsat_auto.lean.out.expected
  1796. grind_cutsat_commring.lean
  1797. grind_cutsat_cooper.lean
  1798. grind_cutsat_cooper.lean.out.expected
  1799. grind_cutsat_decompose.lean
  1800. grind_cutsat_diseq_1.lean
  1801. grind_cutsat_diseq_1.lean.out.expected
  1802. grind_cutsat_diseq_2.lean
  1803. grind_cutsat_diseq_2.lean.out.expected
  1804. grind_cutsat_diseq_3.lean
  1805. grind_cutsat_diseq_3.lean.out.expected
  1806. grind_cutsat_diseq_cooper.lean
  1807. grind_cutsat_diseq_cooper.lean.out.expected
  1808. grind_cutsat_div_1.lean
  1809. grind_cutsat_div_1.lean.out.expected
  1810. grind_cutsat_div_mod.lean
  1811. grind_cutsat_div_mod.lean.out.expected
  1812. grind_cutsat_eq_1.lean
  1813. grind_cutsat_eq_1.lean.out.expected
  1814. grind_cutsat_instances.lean
  1815. grind_cutsat_le_1.lean
  1816. grind_cutsat_le_1.lean.out.expected
  1817. grind_cutsat_le_2.lean
  1818. grind_cutsat_le_2.lean.out.expected
  1819. grind_cutsat_nat_dvd.lean
  1820. grind_cutsat_nat_dvd.lean.out.expected
  1821. grind_cutsat_nat_eq.lean
  1822. grind_cutsat_nat_eq.lean.out.expected
  1823. grind_cutsat_nat_le.lean
  1824. grind_cutsat_nat_le.lean.out.expected
  1825. grind_cutsat_natCast_propagation.lean
  1826. grind_cutsat_omega.lean
  1827. grind_cutsat_pow.lean
  1828. grind_cutsat_proof_term_issue.lean
  1829. grind_cutsat_tests.lean
  1830. grind_cutsat_tests.lean.out.expected
  1831. grind_cutsat_toint_1.lean
  1832. grind_cutsat_trim_context.lean
  1833. grind_cutsat_upper_bug.lean
  1834. grind_cutsat_upper_bug.lean.out.expected
  1835. grind_cutsat_zero.lean
  1836. grind_decide_bool_issues.lean
  1837. grind_decide_bool_issues.lean.out.expected
  1838. grind_def_eq_inv_issue.lean
  1839. grind_dep_match_overlap.lean
  1840. grind_diseq.lean
  1841. grind_diseq_cancel_var_bug.lean
  1842. grind_dvd_propagate_issue.lean
  1843. grind_dvd_propagate_issue.lean.out.expected
  1844. grind_ematch1.lean
  1845. grind_ematch1.lean.out.expected
  1846. grind_ematch2.lean
  1847. grind_ematch2.lean.out.expected
  1848. grind_ematch_diag.lean
  1849. grind_ematch_gen_pattern.lean
  1850. grind_ematch_gen_pattern.lean.out.expected
  1851. grind_ematch_ground_implicit_inst.lean
  1852. grind_ematch_patterns.lean
  1853. grind_ematch_patterns.lean.out.expected
  1854. grind_ematch_theorem_activation.lean
  1855. grind_ematch_theorem_activation.lean.out.expected
  1856. grind_ematch_type_error.lean
  1857. grind_eq.lean
  1858. grind_eq.lean.out.expected
  1859. grind_eq_bwd.lean
  1860. grind_eq_bwd.lean.out.expected
  1861. grind_eq_bwd_pat_bug.lean
  1862. grind_eq_bwd_pat_bug.lean.out.expected
  1863. grind_eq_false_of_imp_eq_false.lean
  1864. grind_eq_false_of_imp_eq_false.lean.out.expected
  1865. grind_eq_pattern.lean
  1866. grind_eqc_inv_issue.lean
  1867. grind_eqres_bug.lean
  1868. grind_erase_attr.lean
  1869. grind_erase_attr.lean.out.expected
  1870. grind_eta.lean
  1871. grind_eta_struct_internalize.lean
  1872. grind_eta_struct_internalize.lean.out.expected
  1873. grind_etaStruct.lean
  1874. grind_eval_suggest.lean
  1875. grind_eval_suggest.lean.out.expected
  1876. grind_exfalso.lean
  1877. grind_ExtTreeSet.lean
  1878. grind_fastEraseDups.lean
  1879. grind_field_div.lean
  1880. grind_field_norm.lean
  1881. grind_field_norm_2.lean
  1882. grind_field_panic.lean
  1883. grind_field_panic.lean.out.expected
  1884. grind_fin.lean
  1885. grind_fin_bug.lean
  1886. grind_fin_zero.lean
  1887. grind_finish_trace.lean
  1888. grind_finish_trace.lean.out.expected
  1889. grind_finVal.lean
  1890. grind_fun_singleton.lean
  1891. grind_funCC.lean
  1892. grind_funext.lean
  1893. grind_getElem.lean
  1894. grind_getElem.lean.out.expected
  1895. grind_getLast_dropLast.lean
  1896. grind_ground_pat_issue.lean
  1897. grind_ground_pat_issue.lean.out.expected
  1898. grind_ground_thm.lean
  1899. grind_guide.lean
  1900. grind_guide.lean.out.ignored
  1901. grind_guide_2.lean
  1902. grind_guide_2.lean.out.expected
  1903. grind_hashmap_list.lean
  1904. grind_hashmap_list.lean.out.expected
  1905. grind_hcongr.lean
  1906. grind_heapsort.lean
  1907. grind_heapsort.lean.out.expected
  1908. grind_heartbeats.lean
  1909. grind_heartbeats.lean.out.expected
  1910. grind_heq_proof_issue.lean
  1911. grind_human_eval_114.lean
  1912. grind_hyper_ex.lean
  1913. grind_ignore_impl_detail.lean
  1914. grind_implies.lean
  1915. grind_indexmap.lean
  1916. grind_indexmap_pre.lean
  1917. grind_indexmap_pre.lean.out.expected
  1918. grind_indexmap_trace.lean
  1919. grind_indexmap_trace.lean.out.expected
  1920. grind_inj.lean
  1921. grind_inj2.lean
  1922. grind_inj2.lean.out.expected
  1923. grind_inj_clear_issue.lean
  1924. grind_inst_mvars_issue.lean
  1925. grind_inst_mvars_issue.lean.out.expected
  1926. grind_intcast_natcast.lean
  1927. grind_interactive.lean
  1928. grind_interactive.lean.out.expected
  1929. grind_interactive_2.lean
  1930. grind_interactive_2.lean.out.expected
  1931. grind_internalize_bitvec_lit.lean
  1932. grind_internalize_bitvec_lit.lean.out.expected
  1933. grind_intmodule_eq_prop.lean
  1934. grind_issue_9125.lean
  1935. grind_issue_9187.lean
  1936. grind_ite.lean
  1937. grind_ite_congr.lean
  1938. grind_ite_parent.lean
  1939. grind_ite_split_issue.lean
  1940. grind_ite_trace.lean
  1941. grind_ite_trace.lean.out.expected
  1942. grind_ite_unused_match.lean
  1943. grind_ite_unused_match.lean.out.expected
  1944. grind_lawful_eq_cmp.lean
  1945. grind_lax.lean
  1946. grind_lax.lean.out.expected
  1947. grind_lazy_ite.lean
  1948. grind_lazy_ite.lean.out.expected
  1949. grind_lex.lean
  1950. grind_lia_regression.lean
  1951. grind_linarith_1.lean
  1952. grind_linarith_1.lean.out.expected
  1953. grind_linarith_2.lean
  1954. grind_linarith_2.lean.out.expected
  1955. grind_linarith_rational.lean
  1956. grind_linarith_spurious_issues.lean
  1957. grind_linarith_trim_context.lean
  1958. grind_linearize.lean
  1959. grind_lint_1.lean
  1960. grind_lint_array.lean
  1961. grind_lint_bitvec.lean
  1962. grind_lint_list.lean
  1963. grind_lint_misc.lean
  1964. grind_lint_std_hashmap.lean
  1965. grind_lint_std_misc.lean
  1966. grind_lint_std_treemap.lean
  1967. grind_list.lean
  1968. grind_list.lean.out.expected
  1969. grind_list3.lean
  1970. grind_list_count.lean
  1971. grind_list_drop_take.lean
  1972. grind_list_erase.lean
  1973. grind_list_find.lean
  1974. grind_list_issue.lean
  1975. grind_list_issue.lean.out.expected
  1976. grind_list_perm.lean
  1977. grind_list_sublist.lean
  1978. grind_local_hyps.lean
  1979. grind_locals.lean
  1980. grind_locals_module.lean
  1981. grind_lookahead.lean
  1982. grind_lookahead.lean.out.expected
  1983. grind_many_eqs.lean
  1984. grind_map.lean
  1985. grind_mark_nested_proofs_bug.lean
  1986. grind_match1.lean
  1987. grind_match1.lean.out.expected
  1988. grind_match2.lean
  1989. grind_match2.lean.out.expected
  1990. grind_match_cond_contra.lean
  1991. grind_match_cond_issue.lean
  1992. grind_match_cond_split.lean
  1993. grind_match_eq_propagation.lean
  1994. grind_match_with_eq.lean
  1995. grind_mbtc_1.lean
  1996. grind_mbtc_1.lean.out.expected
  1997. grind_mbtc_bad_splits.lean
  1998. grind_min.lean
  1999. grind_module_eqs.lean
  2000. grind_module_normalization.lean
  2001. grind_module_relations.lean
  2002. grind_mon_order.lean
  2003. grind_mon_order.lean.out.expected
  2004. grind_mvar.lean
  2005. grind_mvar.lean.out.expected
  2006. grind_mvar_hyps.lean
  2007. grind_nat_bitwise.lean
  2008. grind_nat_module.lean
  2009. grind_nat_module_2.lean
  2010. grind_nat_module_norm.lean
  2011. grind_nat_semiring.lean
  2012. grind_nat_sub_encoding.lean
  2013. grind_natCast.lean
  2014. grind_natCast_intCast.lean
  2015. grind_natCast_issue.lean
  2016. grind_natCast_nonneg_ring.lean
  2017. grind_nested_mdata.lean
  2018. grind_nested_proof_issue.lean
  2019. grind_nested_proofs.lean
  2020. grind_nested_proofs.lean.out.expected
  2021. grind_nochrono.lean
  2022. grind_noncomm_ring.lean
  2023. grind_noncomm_semiring.lean
  2024. grind_nonforall_params.lean
  2025. grind_nonlinear_occ_issue.lean
  2026. grind_norm.lean
  2027. grind_norm_levels.lean
  2028. grind_not_internalized.lean
  2029. grind_offset.lean
  2030. grind_offset.lean.out.expected
  2031. grind_omega_examples.lean
  2032. grind_omega_tests.lean
  2033. grind_one_mul.lean
  2034. grind_one_mul.lean.out.expected
  2035. grind_option.lean
  2036. grind_ord_module.lean
  2037. grind_order_1.lean
  2038. grind_order_2.lean
  2039. grind_order_3.lean
  2040. grind_order_eq.lean
  2041. grind_order_issue.lean
  2042. grind_order_propagation.lean
  2043. grind_over_applied_nestedProof.lean
  2044. grind_overapplied_ite.lean
  2045. grind_overapplied_ite.lean.out.expected
  2046. grind_palindrome2.lean
  2047. grind_palindromes.lean
  2048. grind_palindromes.lean.out.expected
  2049. grind_panic_invariant.lean
  2050. grind_panic_invariant.lean.out.expected
  2051. grind_params.lean
  2052. grind_params.lean.out.expected
  2053. grind_pat_sel.lean
  2054. grind_pattern1.lean
  2055. grind_pattern2.lean
  2056. grind_pattern2.lean.out.expected
  2057. grind_pattern3.lean
  2058. grind_pattern_cnstr.lean
  2059. grind_pattern_cnstr.lean.out.expected
  2060. grind_pattern_cnstr_2.lean
  2061. grind_pattern_inference_issue.lean
  2062. grind_pattern_proj.lean
  2063. grind_pattern_scoped.lean
  2064. grind_pattern_validation_instance.lean
  2065. grind_Poly_mul_0_bug.lean
  2066. grind_pow_add_semiring.lean
  2067. grind_pow_identity.lean
  2068. grind_pow_inst_issue.lean
  2069. grind_pow_inst_issue.lean.out.expected
  2070. grind_pow_zero.lean
  2071. grind_pp_attr.lean
  2072. grind_pre.lean
  2073. grind_pre.lean.out.expected
  2074. grind_preinstance_set_bug.lean
  2075. grind_preinstance_set_bug.lean.out.expected
  2076. grind_preord_module.lean
  2077. grind_primes.lean
  2078. grind_prod.lean
  2079. grind_product_eta_and_split.lean
  2080. grind_proof_perf_issue.lean
  2081. grind_prop_arrow.lean
  2082. grind_prop_arrow.lean.out.expected
  2083. grind_prop_inst.lean
  2084. grind_proveEqIssue.lean
  2085. grind_proveEqIssue.lean.out.expected
  2086. grind_qsort.lean
  2087. grind_qsort.lean.out.expected
  2088. grind_question_mark_suggestions.lean
  2089. grind_rat.lean
  2090. grind_reducible.lean
  2091. grind_reducible.lean.out.expected
  2092. grind_refl_cmp.lean
  2093. grind_regression.lean
  2094. grind_regression.lean.out.expected
  2095. grind_ring_1.lean
  2096. grind_ring_1.lean.out.expected
  2097. grind_ring_2.lean
  2098. grind_ring_2.lean.out.expected
  2099. grind_ring_3.lean
  2100. grind_ring_4.lean
  2101. grind_ring_degree_explosion.lean
  2102. grind_ring_norm_ring_proof.lean
  2103. grind_ring_op_sanity_checks.lean
  2104. grind_ring_trim_context.lean
  2105. grind_section_var.lean
  2106. grind_semiring.lean
  2107. grind_semiring_norm.lean
  2108. grind_semiring_norm_regression.lean
  2109. grind_semiring_norm_regression.lean.out.expected
  2110. grind_set_config.lean
  2111. grind_set_config.lean.out.expected
  2112. grind_shelf.lean
  2113. grind_smul_issue.lean
  2114. grind_som1.lean
  2115. grind_sort_eqc.lean
  2116. grind_sort_eqc.lean.out.expected
  2117. grind_sort_intern.lean
  2118. grind_split.lean
  2119. grind_split.lean.out.expected
  2120. grind_split_arith_imp.lean
  2121. grind_split_arith_imp.lean.out.expected
  2122. grind_split_data.lean
  2123. grind_split_issue.lean
  2124. grind_split_issue.lean.out.expected
  2125. grind_spoly.lean
  2126. grind_suggestions.lean
  2127. grind_sym_prio.lean
  2128. grind_sym_prio.lean.out.expected
  2129. grind_t1.lean
  2130. grind_t1.lean.out.expected
  2131. grind_toint_instances.lean
  2132. grind_toint_instances.lean.out.expected
  2133. grind_toInt_issue.lean
  2134. grind_toInt_mbtc.lean
  2135. grind_trace.lean
  2136. grind_trace.lean.out.expected
  2137. grind_trace_local_dot_notation.lean
  2138. grind_trace_term_params.lean
  2139. grind_trig.lean
  2140. grind_trig.lean.out.expected
  2141. grind_try_exact.lean
  2142. grind_try_exact.lean.out.expected
  2143. grind_try_extend.lean
  2144. grind_try_trace.lean
  2145. grind_try_trace.lean.out.expected
  2146. grind_unfold_reducible_issue.lean
  2147. grind_unfold_reducible_regression.lean
  2148. grind_unfold_reducible_regression.lean.out.expected
  2149. grind_univ_poly_ground_pattern.lean
  2150. grind_universe_polymorphism.lean
  2151. grind_unnecessary_hypothesis.lean
  2152. grind_unused_lemmas.lean
  2153. grind_usr.lean
  2154. grind_usr.lean.out.expected
  2155. grind_vector.lean
  2156. grind_warn_param.lean
  2157. grindDeprecated.lean
  2158. gring_11543.lean
  2159. gring_11543.lean.out.expected
  2160. guard_expr.lean
  2161. guard_msgs.lean
  2162. guard_msgs.lean.init.sh
  2163. guardexpr.lean
  2164. guessLex.lean
  2165. guessLex.lean.out.expected
  2166. guessLexTricky.lean
  2167. guessLexTricky.lean.out.expected
  2168. guessLexTricky2.lean
  2169. guessLexTricky2.lean.out.expected
  2170. handleLocking.lean
  2171. handleLocking.lean.before.sh
  2172. hasExposedBody.lean
  2173. hashableBug.lean
  2174. hashmap-implicits.lean
  2175. hashmap-toList-simps.lean
  2176. hashmap.lean
  2177. hasNotBit.lean
  2178. haveDestruct.lean
  2179. haveI.lean
  2180. haveI.lean.out.expected
  2181. haveTactic.lean
  2182. hcongr.lean
  2183. hcongr.lean.out.expected
  2184. heapSort.lean
  2185. heapSort.lean.out.expected
  2186. heqSubst.lean
  2187. hexnum.lean
  2188. hinj_thm.lean
  2189. hintPreviewSpan.lean
  2190. hintSuggestionMessage.lean
  2191. hintWordDiff.lean
  2192. hlistOverload.lean
  2193. hmul2.lean
  2194. hmul2.lean.out.expected
  2195. hmulDefaultInstance.lean
  2196. hmulDefaultInstance.lean.out.expected
  2197. hpow.lean
  2198. hpow.lean.out.expected
  2199. idbg_basic.lean
  2200. idbg_e2e.lean
  2201. idbg_e2e.lean.out.expected
  2202. idSuggestEvery.lean
  2203. idSuggestPostHoc.lean
  2204. idSuggestShort.lean
  2205. idSuggestStandalone.lean
  2206. ifcongr.lean
  2207. ifcongr.lean.out.expected
  2208. iffRefl.lean
  2209. ifThenElseIssue.lean
  2210. ifThenElseIssue2.lean
  2211. impByNameResolution.lean
  2212. impLambdaTac.lean
  2213. implDetailBinder.lean
  2214. implicit_reducible_list_length.lean
  2215. implicit_reducible_list_length.lean.out.expected
  2216. implicitApplyIssue.lean
  2217. implicitLambdaLocalWithoutType.lean
  2218. implicitReducibleFunctorComp.lean
  2219. implicitReducibleFunctorComp.lean.out.expected
  2220. implicitRflProofs.lean
  2221. implicitTypesRecCoe.lean
  2222. importStructure.lean
  2223. impossibleInstance.lean
  2224. impossibleTactic.lean
  2225. inaccessibleAnnotDefEqIssue.lean
  2226. inaccessibleAnnotDefEqIssue.lean.out.expected
  2227. incmd.lean
  2228. incmd.lean.out.expected
  2229. ind_cmd_bug.lean
  2230. ind_whnf.lean
  2231. ind_whnf2.lean
  2232. index_variables_linter.lean
  2233. indPredRecursion.lean
  2234. induction1.lean
  2235. inductionAltExplicit.lean
  2236. inductionCheckAltNames.lean
  2237. inductionComplexMotive.lean
  2238. inductionLetIssue.lean
  2239. inductionParse.lean
  2240. inductionTacticBug.lean
  2241. inductive1.lean
  2242. inductive1.lean.out.expected
  2243. inductive2.lean
  2244. inductive2.lean.out.expected
  2245. inductive_mutual.lean
  2246. inductive_pred.lean
  2247. inductive_pred.lean.out.expected
  2248. inductive_rec_proj.lean
  2249. inductive_typestar.lean
  2250. inductive_univ.lean
  2251. inductiveBinderUpdates.lean
  2252. inductiveIndicesIssue.lean
  2253. inductiveParamMismatchError.lean
  2254. indUsingLet.lean
  2255. indUsingTerm.lean
  2256. inferForallTypeLCNF.lean
  2257. inferForallTypeLCNF.lean.out.expected
  2258. inferInstanceAs.lean
  2259. inferTypeFailure.lean
  2260. infixprio.lean
  2261. info_trees.lean
  2262. infoFromFailure.lean
  2263. initializeNonemptyErrorMsg.lean
  2264. initModule.lean
  2265. inj1.lean
  2266. inj2.lean
  2267. injectionBug.lean
  2268. injections1.lean
  2269. injectionsIssue.lean
  2270. injective.lean
  2271. injHEq.lean
  2272. injIssue.lean
  2273. injSimp.lean
  2274. inline_fn.lean
  2275. inlineApp.lean
  2276. inlineExpr.lean
  2277. inlineIfReduceLCNF.lean
  2278. inlineIfReduceLCNF.lean.out.ignored
  2279. inlineIssue.lean
  2280. inlineLCNFIssue.lean
  2281. inlineLCNFIssue.lean.out.ignored
  2282. inlineLoop.lean
  2283. inlineProjInstIssue.lean
  2284. inliner_loop.lean
  2285. inlineWithNestedRecIssue.lean
  2286. inlineWithNestedRecIssue.lean.out.ignored
  2287. inst.lean
  2288. inst.lean.out.expected
  2289. instanceIssues.lean
  2290. instanceReducibility.lean
  2291. instanceReducible.lean
  2292. instances.lean
  2293. instances.lean.out.ignored
  2294. instanceUsingFalse.lean
  2295. instanceWhere.lean
  2296. instanceWhereDecls.lean
  2297. instantiateMVarsCrossScope.lean
  2298. instantiateMVarsShadow.lean
  2299. instantiateMVarsSharing.lean
  2300. instantiateRevBetaS.lean
  2301. instEtaIssue.lean
  2302. instPatVar.lean
  2303. instprio.lean
  2304. instuniv.lean
  2305. instuniv.lean.out.expected
  2306. int_complement_shiftRight.lean
  2307. int_div_mod.lean
  2308. int_to_nat_bug.lean
  2309. int_toBitVec.lean
  2310. internalizeCasesIssue.lean
  2311. interp.lean
  2312. interp.lean.out.expected
  2313. interp2.lean
  2314. interp2.lean.out.expected
  2315. intModBug.lean
  2316. intModBug.lean.out.expected
  2317. intNegSucc.lean
  2318. intNegSucc.lean.out.expected
  2319. intro.lean
  2320. introLetBug.lean
  2321. introLetBug.lean.out.expected
  2322. introLetFun.lean
  2323. intromacro.lean
  2324. invalid_dotted_identifier_prop.lean
  2325. invalid_field_notation_function.lean
  2326. invalid_field_notation_function.lean.out.expected
  2327. invalid_field_notation_mvar.lean
  2328. invalid_field_notation_unusable_param.lean
  2329. invalidProjection.lean
  2330. invalidTupleProjHints.lean
  2331. IO_test.lean
  2332. IO_test.lean.before.sh
  2333. ioNulBytes.lean
  2334. ioRandomBytes.lean
  2335. ioRandomBytes.lean.out.ignored
  2336. IRbug.lean
  2337. IRbug.lean.out.expected
  2338. irCompilerBug.lean
  2339. irreducibleIssue.lean
  2340. isDefEqCheckAssignmentBug.lean
  2341. isDefEqCheckAssignmentBug.lean.out.expected
  2342. isDefEqConstApproxIssue.lean
  2343. isDefEqIssue.lean
  2344. isDefEqMVarSelfIssue.lean
  2345. isDefEqMVarSelfIssue.lean.out.expected
  2346. isDefEqPerfIssue.lean
  2347. isDefEqPerfIssue.lean.out.expected
  2348. isDefEqProjIssue.lean
  2349. isDefEqProjPerfIssue.lean
  2350. isDefEqProjPerfIssue.lean.out.expected
  2351. isInstanceCongrRegression.lean
  2352. isNoncomputable.lean
  2353. isNoncomputable.lean.out.expected
  2354. issue10132.lean
  2355. issue10195.lean
  2356. issue10299.lean
  2357. issue10329.lean
  2358. issue10353.lean
  2359. issue10416.lean
  2360. issue10424.lean
  2361. issue10431.lean
  2362. issue10573.lean
  2363. issue10651.lean
  2364. issue10678.lean
  2365. issue10683.lean
  2366. issue10705.lean
  2367. issue10710.lean
  2368. issue10721.lean
  2369. issue10723.lean
  2370. issue10749.lean
  2371. issue10775.lean
  2372. issue10781.lean
  2373. issue10792.lean
  2374. issue10794.lean
  2375. issue10821.lean
  2376. issue10895.lean
  2377. issue10976.lean
  2378. issue11181.lean
  2379. issue11183.lean
  2380. issue11186.lean
  2381. issue11211.lean
  2382. issue11221.lean
  2383. issue11342.lean
  2384. issue11449.lean
  2385. issue11450.lean
  2386. issue11560.lean
  2387. issue11610.lean
  2388. issue11655.lean
  2389. issue11665.lean
  2390. issue11695.lean
  2391. issue12240.lean
  2392. issue12268.lean
  2393. issue12398.lean
  2394. issue12404.lean
  2395. issue12495.lean
  2396. issue12495.lean.out.expected
  2397. issue12543.lean
  2398. issue12630.lean
  2399. issue12630.lean.out.expected
  2400. issue12768.lean
  2401. issue12804.lean
  2402. issue12819.lean
  2403. issue12826.lean
  2404. issue12846.lean
  2405. issue13015.lean
  2406. issue13373.lean
  2407. issue13444.lean
  2408. issue13691.lean
  2409. issue13705_dedup.lean
  2410. issue13705_nested.lean
  2411. issue13705_nested.lean.out.expected
  2412. issue13729.lean
  2413. issue2102.lean
  2414. issue2108.lean
  2415. issue2113.lean
  2416. issue2171.lean
  2417. issue2237.lean
  2418. issue2628.lean
  2419. issue2628.lean.out.expected
  2420. issue2883.lean
  2421. issue2925.lean
  2422. issue2962.lean
  2423. issue2975.lean
  2424. issue2975.lean.out.expected
  2425. issue2981.lean
  2426. issue2981.lean.out.expected
  2427. issue2982.lean
  2428. issue3175.lean
  2429. issue3204.lean
  2430. issue3212.lean
  2431. issue3212.lean.out.expected
  2432. issue3770.lean
  2433. issue3848.lean
  2434. issue4063.lean
  2435. issue4146.lean
  2436. issue4394.lean
  2437. issue4540.lean
  2438. issue4650.lean
  2439. issue4671.lean
  2440. issue4684.lean
  2441. issue4726.lean
  2442. issue5027.lean
  2443. issue5061.lean
  2444. issue5347.lean
  2445. issue5384.lean
  2446. issue5562.lean
  2447. issue5602.lean
  2448. issue5630.lean
  2449. issue5630.lean.out.expected
  2450. issue5661.lean
  2451. issue5699.lean
  2452. issue5726.lean
  2453. issue5767.lean
  2454. issue5767.lean.out.expected
  2455. issue5828.lean
  2456. issue5836.lean
  2457. issue5903.lean
  2458. issue6015.lean
  2459. issue6281.lean
  2460. issue6281.lean.out.expected
  2461. issue6531.lean
  2462. issue6550.lean
  2463. issue6592.lean
  2464. issue6786.lean
  2465. issue7318.lean
  2466. issue7322.lean
  2467. issue7332.lean
  2468. issue7383.lean
  2469. issue7383.lean.out.expected
  2470. issue7408.lean
  2471. issue7550.lean
  2472. issue7826.lean
  2473. issue7826.lean.out.expected
  2474. issue7826a.lean
  2475. issue8093.lean
  2476. issue8098.lean
  2477. issue8103.lean
  2478. issue8107.lean
  2479. issue8195.lean
  2480. issue8213.lean
  2481. issue8257.lean
  2482. issue8274.lean
  2483. issue8293.lean
  2484. issue8360.lean
  2485. issue8490.lean
  2486. issue8939.lean
  2487. issue8939wf.lean
  2488. issue8939wf.lean.out.expected
  2489. issue8962.lean
  2490. issue8969.lean
  2491. issue9018.lean
  2492. issue9462.lean
  2493. issue9646.lean
  2494. issue9844.lean
  2495. issue9846.lean
  2496. ite_dsimproc.lean
  2497. iterators.lean
  2498. james1.lean
  2499. james1.lean.out.expected
  2500. jason1.lean
  2501. jpCasesDiscrM.lean
  2502. jpCasesDiscrM.lean.out.expected
  2503. jpCasesNary.lean
  2504. jpCasesNary.lean.out.expected
  2505. jpClosureIssue.lean
  2506. jpClosureIssue.lean.out.expected
  2507. jpVoidArgs.lean
  2508. json.lean
  2509. json.lean.out.expected
  2510. json2.lean
  2511. json_empty.lean
  2512. jsonSurrogates.lean
  2513. kernel1.lean
  2514. kernel2.lean
  2515. kernel_maxheartbeats.lean
  2516. kernelBacktrack.lean
  2517. kernelBacktrack.lean.out.expected
  2518. kernelErrorFollowup.lean
  2519. kernelInterrupt.lean
  2520. kevin.lean
  2521. keyAttrErase.lean
  2522. keyAttrErase.lean.out.expected
  2523. krivine.lean
  2524. kronRWIssue.lean
  2525. kronRWIssue.lean.out.expected
  2526. KyleAlg.lean
  2527. KyleAlg.lean.out.expected
  2528. KyleAlgAbbrev.lean
  2529. lambdaLiftCache.lean
  2530. lambdaLiftCache.lean.out.expected
  2531. lazyListRotateUnfoldProof.lean
  2532. lazyListRotateUnfoldProof.lean.out.expected
  2533. lazylistThunk.lean
  2534. lazySeq.lean
  2535. lazySeq.lean.out.expected
  2536. lazyUnfoldingPerfIssue.lean
  2537. lazyUnfoldingPerfIssue.lean.out.expected
  2538. lcnf2.lean
  2539. lcnf2.lean.out.ignored
  2540. lcnf3.lean
  2541. lcnf_borrow_expected_type.lean
  2542. lcnf_export_borrow_error.lean
  2543. lcnf_simp_let.lean
  2544. lcnfBinderNameBug.lean
  2545. lcnfCache.lean
  2546. lcnfCache.lean.out.expected
  2547. lcnfCastIssue.lean
  2548. lcnfCheckIssue.lean
  2549. lcnfCheckIssue.lean.out.ignored
  2550. lcnfErasure.lean
  2551. lcnfInferProjTypeBug.lean
  2552. lcnfInferProjTypeBug.lean.out.ignored
  2553. lcnfInferProjTypeIssue.lean
  2554. lcnfInferProjTypeIssue.lean.out.ignored
  2555. lcnfInliningIssue.lean
  2556. lcnfInliningIssue.lean.out.ignored
  2557. lcnfIssue.lean
  2558. lcnfIssue.lean.out.ignored
  2559. lcnfTypes.lean
  2560. lcnfTypes.lean.out.expected
  2561. LE.lean
  2562. LE.lean.out.expected
  2563. lean3_zulip_issues_1.lean
  2564. lean3RefineBug.lean
  2565. lean3RefineBug.lean.out.expected
  2566. lean_nat_bitwise.lean
  2567. lean_nat_gcd.lean
  2568. left_right.lean
  2569. lemma.lean
  2570. let_Issue.lean
  2571. letBRecOnIssue.lean
  2572. letDeclSimp.lean
  2573. letFun.lean
  2574. letFun.lean.out.expected
  2575. letFunUnusedVarBug.lean
  2576. letMVar.lean
  2577. letMVar.lean.out.expected
  2578. letNonDep.lean
  2579. letrecInProofs.lean
  2580. letrecInThm.lean
  2581. letRecTheorem.lean
  2582. letRecTheorem.lean.out.expected
  2583. letrecWFIssue.lean
  2584. letToHave.lean
  2585. letToHaveCleanup.lean
  2586. level.lean
  2587. levelNamesInTacticMode.lean
  2588. levelNGen.lean
  2589. levelNGen.lean.out.expected
  2590. levenshtein.lean
  2591. lex.lean
  2592. lia_attr.lean
  2593. lia_order_bug.lean
  2594. lia_with_cases.lean
  2595. liaByRefl.lean
  2596. library_search_all.lean
  2597. library_search_grind.lean
  2598. library_search_grind.lean.out.expected
  2599. library_suggestions.lean
  2600. library_suggestions.lean.out.ignored
  2601. library_suggestions_deprecated.lean
  2602. library_suggestions_import.lean
  2603. library_suggestions_local.lean
  2604. library_suggestions_mepo.lean
  2605. library_suggestions_mepo.lean.out.ignored
  2606. library_suggestions_mepo_order.lean
  2607. library_suggestions_mepo_order.lean.out.expected
  2608. library_suggestions_override.lean
  2609. library_suggestions_persistent.lean
  2610. library_suggestions_persistent_module.lean
  2611. library_suggestions_private.lean
  2612. library_suggestions_relevant_constants.lean
  2613. library_suggestions_relevant_constants.lean.out.expected
  2614. library_suggestions_sine_qua_non.lean
  2615. librarySearch.lean
  2616. librarySearch.lean.out.expected
  2617. libuv.lean
  2618. lift_lets.lean
  2619. LiftMethodIssue.lean
  2620. linearByRefl.lean
  2621. linearCategory_perf_issue.lean
  2622. linearCategory_perf_issue.lean.out.expected
  2623. linearDecEq.lean
  2624. linearNoConfusion.lean
  2625. linterCheckUnivs.lean
  2626. linterCoe.lean
  2627. linterMissingDocs.lean
  2628. linterMissingDocs.lean.out.expected
  2629. linterRedundantExpose.lean
  2630. linterSuspiciousUnexpanderPatterns.lean
  2631. linterSuspiciousUnexpanderPatterns.lean.out.expected
  2632. linterTacticCheckInstances.lean
  2633. linterUnusedDecidableInType.lean
  2634. list_monadic_functions.lean
  2635. list_monadic_functions.lean.out.expected
  2636. list_simp.lean
  2637. list_variables_linter.lean
  2638. listDecEq.lean
  2639. listLength.lean
  2640. listLength.lean.out.expected
  2641. listtostring.lean
  2642. listtostring.lean.out.expected
  2643. lit_values.lean
  2644. lit_values.lean.out.expected
  2645. litToCtor.lean
  2646. localGlobalNotation.lean
  2647. localNameResolutionWithProj.lean
  2648. localNotationPP.lean
  2649. localNotationPP.lean.out.expected
  2650. localParsers.lean
  2651. lossy_casts.lean
  2652. lrat_roundtrip.lean
  2653. lvl1.lean
  2654. lvl1.lean.out.expected
  2655. macro.lean
  2656. macro2.lean
  2657. macro3.lean
  2658. macro_macro.lean
  2659. macro_macro.lean.out.expected
  2660. macroElabRulesIssue1.lean
  2661. macroElabRulesIssue1.lean.out.expected
  2662. macroid.lean
  2663. macroid.lean.out.expected
  2664. macroParams.lean
  2665. macroResolveName.lean
  2666. macroResolveName.lean.out.expected
  2667. macroscopes.lean
  2668. macroscopes.lean.out.expected
  2669. macroTrace.lean
  2670. macroTrace.lean.out.expected
  2671. magical.lean
  2672. mainIncorrectType1.lean
  2673. mainIncorrectType2.lean
  2674. mainIncorrectType3.lean
  2675. mainIncorrectType4.lean
  2676. mainIncorrectType5.lean
  2677. mainType1.lean
  2678. mainType2.lean
  2679. mainType3.lean
  2680. mainType4.lean
  2681. mainType5.lean
  2682. mainType6.lean
  2683. mangling.lean
  2684. manyAritySyntax.lean
  2685. mapTR.lean
  2686. match1.lean
  2687. match2.lean
  2688. match2.lean.out.ignored
  2689. match3.lean
  2690. match3.lean.out.expected
  2691. match4.lean
  2692. match4.lean.out.expected
  2693. match_ctorIdx.lean
  2694. match_eqns_bug.lean
  2695. match_expose_implicit_reducible.lean
  2696. match_expr.lean
  2697. match_expr_expected_type_issue.lean
  2698. match_expr_meta_modifier.lean
  2699. match_expr_perf.lean
  2700. match_float.lean
  2701. match_int_lit_issue.lean
  2702. match_lit_fin_cover.lean
  2703. match_lit_issues.lean
  2704. match_lit_issues.lean.out.expected
  2705. match_lit_regression.lean
  2706. match_lit_regression.lean.out.expected
  2707. match_nat.lean
  2708. match_unit.lean
  2709. matchApp.lean
  2710. matchApp.lean.out.expected
  2711. matchArrayLit.lean
  2712. matchCongrEqns.lean
  2713. matchDiscrType.lean
  2714. matchEqnsHEqIssue.lean
  2715. matchEqnsHEqIssue.lean.out.expected
  2716. matchEqs.lean
  2717. matchEqs.lean.out.expected
  2718. matchEqsBug.lean
  2719. matchEqsBug.lean.out.expected
  2720. matcherElimUniv.lean
  2721. matchGenBug.lean
  2722. matchGenBug.lean.out.expected
  2723. matchGenIssue.lean
  2724. matchMissingCase.lean
  2725. matchMultAlt.lean
  2726. matchMultAlt.lean.out.expected
  2727. matchNoPostponing.lean
  2728. matchOfNatIssue.lean
  2729. matchOfNatIssue.lean.out.expected
  2730. matchPatternInsideBinders.lean
  2731. matchPatternInsideBinders.lean.out.expected
  2732. matchPatternPartialApp.lean
  2733. matchPatternPartialApp.lean.out.expected
  2734. matchPatternVarErrors.lean
  2735. matchRw.lean
  2736. matchSparse.lean
  2737. matchSparse2.lean
  2738. matchtac.lean
  2739. matchtac.lean.out.expected
  2740. matchUnifyBug.lean
  2741. matchunit.lean
  2742. matchunit.lean.out.expected
  2743. matchVarIssue.lean
  2744. matchWithSearch.lean
  2745. mathlibetaissue.lean
  2746. mathlibetaissue.lean.out.expected
  2747. mathport18.lean
  2748. mathport18.lean.out.expected
  2749. mathport_issue16.lean
  2750. mathport_issue16.lean.out.expected
  2751. matrix.lean
  2752. maxSuggestionsTest.lean
  2753. may_postpone_tc.lean
  2754. maze.lean
  2755. mergeSort.lean
  2756. mergeSortCPDT.lean
  2757. messageKind.lean
  2758. meta.lean
  2759. meta1.lean
  2760. meta2.lean
  2761. meta2.lean.out.ignored
  2762. meta3.lean
  2763. meta4.lean
  2764. meta5.lean
  2765. meta6.lean
  2766. meta6.lean.out.expected
  2767. meta7.lean
  2768. meta7.lean.out.ignored
  2769. methodSpecs.lean
  2770. methodSpecsDeriving.lean
  2771. methodsRetInhabited.lean
  2772. mightBeDerivable.lean
  2773. Miller1.lean
  2774. mintroErrorMessage.lean
  2775. missingDeclName.lean
  2776. missingDocsTacticAlt.lean
  2777. missingExplicitWithForwardNamedDep.lean
  2778. missingSizeOfArrayGetThm.lean
  2779. mixedMacroRules.lean
  2780. mixedMacroRules.lean.out.expected
  2781. mixfix.lean
  2782. mjissue.lean
  2783. modAsClasses.lean
  2784. moduleDoc.lean
  2785. moduleDoc.lean.out.expected
  2786. moduleHeaderLeadingWhitespace.lean
  2787. monadCache.lean
  2788. monadCache.lean.out.expected
  2789. monadControl.lean
  2790. MonadControl_tutorial.lean
  2791. monotone.lean
  2792. more_jps.lean
  2793. mspecInvariantInstantiation.lean
  2794. mspecInvariantInstantiation.lean.out.expected
  2795. mspecNoAssignSyntheticOpaque.lean
  2796. mul_match_pattern.lean
  2797. mulcomm.lean
  2798. multiTargetCasesInductionIssue.lean
  2799. mut_ind_wf.lean
  2800. mutual_coinduction.lean
  2801. mutual_termination_by_errors.lean
  2802. mutualDefThms.lean
  2803. mutualWithCompositeNames.lean
  2804. mutualWithMacro.lean
  2805. mutualWithNamespaceMacro.lean
  2806. mutwf1.lean
  2807. mutwf2.lean
  2808. mutwf2.lean.out.expected
  2809. mutwf3.lean
  2810. mutwf3.lean.out.expected
  2811. mutwf4.lean
  2812. mutwf4.lean.out.expected
  2813. mvar_fvar.lean
  2814. mvar_fvar.lean.out.expected
  2815. mvcgenInvariantsSuggestions.lean
  2816. mvcgenInvariantsWith.lean
  2817. mvcgenJPs.lean
  2818. mvcgenLocalSpec.lean
  2819. mvcgenPRangeInst.lean
  2820. mvcgenRflReducibility.lean
  2821. mvcgenSimpClassMethod.lean
  2822. mvcgenSplitState.lean
  2823. mvcgenTutorial.lean
  2824. mvcgenUnknownIdent.lean
  2825. mvcgenWithFail.lean
  2826. name_eq_bug.lean
  2827. namelit.lean
  2828. namelit.lean.out.expected
  2829. namePatEqThm.lean
  2830. nameRepr.lean
  2831. nameRepr.lean.out.expected
  2832. namespaceHyg.lean
  2833. namespaceIssue.lean
  2834. namespaceResolution.lean
  2835. nary_nomatch.lean
  2836. nat_mod_defeq.lean
  2837. nativeReflBackdoor.lean
  2838. natlit.lean
  2839. negFloat.lean
  2840. negFloat.lean.out.expected
  2841. nested_inductive.lean
  2842. nested_match_bug.lean
  2843. nested_match_slowdown.lean
  2844. nestedActionDoElem.lean
  2845. nestedActionInMacrosIssue.lean
  2846. nestedActionLegacyElab.lean
  2847. nestedDo.lean
  2848. nestedInductiveConstructions.lean
  2849. nestedInductiveIssue.lean
  2850. nestedInductiveRecType.lean
  2851. nestedInductiveUniverse.lean
  2852. nestedIssueMatch.lean
  2853. nestedIssueMatch.lean.out.expected
  2854. nestedrec.lean
  2855. nestedtc.lean
  2856. nestedtc.lean.out.expected
  2857. nestedTypeFormers.lean
  2858. nestedWF.lean
  2859. nestedWF.lean.out.expected
  2860. net_addr.lean
  2861. networkInterfaces.lean
  2862. never_extract.lean
  2863. new_compiler.lean
  2864. new_frontend2.lean
  2865. new_frontend2.lean.out.expected
  2866. new_inductive.lean
  2867. new_inductive.lean.out.expected
  2868. new_inductive2.lean
  2869. new_inductive2.lean.out.expected
  2870. newdo.lean
  2871. newdo.lean.out.expected
  2872. newfrontend1.lean
  2873. newfrontend1.lean.out.expected
  2874. newfrontend2.lean
  2875. newfrontend2.lean.out.expected
  2876. newfrontend3.lean
  2877. newfrontend3.lean.out.expected
  2878. newfrontend5.lean
  2879. newfrontend5.lean.out.expected
  2880. nicerNestedDos.lean
  2881. no_grind_constProp.lean
  2882. no_grind_constProp.lean.out.ignored
  2883. no_simproc_usize.lean
  2884. no_simproc_usize.lean.out.expected
  2885. noConfusionCtorInjection.lean
  2886. noConfusionCtors.lean
  2887. noErrorUtil.lean
  2888. noFallbackAttr.lean
  2889. nofun1.lean
  2890. noindexAnnotation.lean
  2891. nomatch_regression.lean
  2892. nomatch_tac.lean
  2893. nonClassInstance.lean
  2894. noncomp.lean
  2895. noncompSection.lean
  2896. noncompSection.lean.out.expected
  2897. noncomputable_bug.lean
  2898. noncomputable_decide.lean
  2899. noncomputableUnused.lean
  2900. nondepArrow.lean
  2901. nondepArrow.lean.out.expected
  2902. nonrec.lean
  2903. norm_cast.lean
  2904. notationDelab.lean
  2905. notationDelab.lean.out.expected
  2906. numChars.lean
  2907. obtain.lean
  2908. offsetIssue.lean
  2909. ofIntClamp.lean
  2910. ofNat_class.lean
  2911. ofNatNormNum.lean
  2912. ofNatNormNum.lean.out.expected
  2913. omega.lean
  2914. omega_examples.lean
  2915. omegaCanon.lean
  2916. omegaDischarger.lean
  2917. omegaDischarger.lean.out.expected
  2918. opaqueCodeGen.lean
  2919. openInScopeBug.lean
  2920. openssl.lean
  2921. openTermTactic.lean
  2922. optionDecEq.lean
  2923. optionGetD.lean
  2924. optionGetD.lean.out.expected
  2925. optParam.lean
  2926. or_shortcircuit.lean
  2927. or_shortcircuit.lean.out.expected
  2928. Ord.lean
  2929. order.lean
  2930. order.lean.out.expected
  2931. overAndPartialAppsAtWF.lean
  2932. overAndPartialAppsAtWF.lean.out.expected
  2933. overlappingTokens.lean
  2934. overloaded.lean
  2935. overloaded.lean.out.expected
  2936. overloadsAndDelayedCoercions.lean
  2937. pairsSumToZero.lean
  2938. pairsSumToZero.lean.out.expected
  2939. panicAtCheckAssignment.lean
  2940. parray1.lean
  2941. PArray_forM.lean
  2942. PArray_forM.lean.out.expected
  2943. parseEnd.lean
  2944. parseImportsFastOverlappingComment.lean
  2945. parsePrelude.lean
  2946. parsePrelude.lean.out.expected
  2947. parserAliasShadow.lean
  2948. parserQuot.lean
  2949. parserQuot.lean.out.expected
  2950. partial1.lean
  2951. partial1.lean.out.expected
  2952. partial_fixpoint.lean
  2953. partial_fixpoint_aeneas.lean
  2954. partial_fixpoint_aeneas2.lean
  2955. partial_fixpoint_aeneas2.lean.out.expected
  2956. partial_fixpoint_explicit.lean
  2957. partial_fixpoint_f91.lean
  2958. partial_fixpoint_induct.lean
  2959. partial_fixpoint_monadic.lean
  2960. partial_fixpoint_monotonicity.lean
  2961. partial_fixpoint_mutual.lean
  2962. partial_fixpoint_probability.lean
  2963. partial_fixpoint_prop.lean
  2964. partial_fixpoint_split.lean
  2965. partialApp.lean
  2966. partialDelta.lean
  2967. patbug.lean
  2968. patternInvalidNamedArg.lean
  2969. pendingInstBug.lean
  2970. pendingMVarIssue.lean
  2971. persistent_lint_log.lean
  2972. phashmap_iter.lean
  2973. postponeBinRelIssue.lean
  2974. posView.lean
  2975. pow_exploit.lean
  2976. ppBeta.lean
  2977. ppBeta.lean.out.expected
  2978. ppDeepTerms.lean
  2979. ppDeepTerms.lean.out.expected
  2980. ppExpr.lean
  2981. ppExpr.lean.out.expected
  2982. ppFVarsAnonymous.lean
  2983. PPInstances.lean
  2984. PPInstances.lean.out.expected
  2985. ppite.lean
  2986. ppite.lean.out.expected
  2987. ppLet.lean
  2988. pplevel.lean
  2989. pplevel.lean.out.expected
  2990. ppMaxSteps.lean
  2991. ppMData.lean
  2992. ppMotives.lean
  2993. ppMotives.lean.out.expected
  2994. ppMVars.lean
  2995. ppMVarsDocstrings.lean
  2996. ppNotationCode.lean
  2997. ppNotationCode.lean.out.expected
  2998. ppNumericTypes.lean
  2999. ppOneline.lean
  3000. ppParens.lean
  3001. ppPiBinderNames.lean
  3002. PProd_syntax.lean
  3003. PPRoundtrip.lean
  3004. PPRoundtrip.lean.out.expected
  3005. ppSpaces.lean
  3006. ppSyntax.lean
  3007. ppSyntax.lean.out.expected
  3008. PPTopDownAnalyze.lean
  3009. PPTopDownAnalyze.lean.out.expected
  3010. ppUnicode.lean
  3011. ppUniverses.lean
  3012. ppUsingAnonymousConstructor.lean
  3013. ppVector.lean
  3014. precDSL.lean
  3015. precDSL.lean.out.expected
  3016. prefixTableStep.lean
  3017. prelude-injectivity.lean
  3018. primProjEtaIssue.lean
  3019. primProjEtaIssue.lean.out.expected
  3020. print_cmd.lean
  3021. print_cmd.lean.out.expected
  3022. printEqns.lean
  3023. printPrivate.lean
  3024. printStructure.lean
  3025. prioDSL.lean
  3026. privateCtor.lean
  3027. privateFieldCopyIssue.lean
  3028. privateFieldCopyIssue.lean.out.expected
  3029. privateInPublic.lean
  3030. Process.lean
  3031. Process.lean.out.expected
  3032. processGenDiseqBug.lean
  3033. proj_delta_issue.lean
  3034. projDefEq2.lean
  3035. projWithIrrelevantFields.lean
  3036. projWithNestedIrrelevantFields.lean
  3037. promise.lean
  3038. proofAsSorry.lean
  3039. proofDataConfusionBug.lean
  3040. proofIrrelFVar.lean
  3041. propagateExpectedType.lean
  3042. prv.lean
  3043. prv.lean.out.expected
  3044. prvNameWithMacroScopes.lean
  3045. psumAtWF.lean
  3046. ptrAddr.lean
  3047. ptrAddr.lean.out.ignored
  3048. qed_macro.lean
  3049. qualifiedNamesRec.lean
  3050. quasi_pattern_unification_approx_issue.lean
  3051. quotInd.lean
  3052. quotInd.lean.out.expected
  3053. range.lean
  3054. rangePolymorphic.lean
  3055. Rat.lean
  3056. rat1.lean
  3057. rat1.lean.out.expected
  3058. rational.lean
  3059. rational.lean.out.expected
  3060. rawStrings.lean
  3061. rc_tests.lean
  3062. rcases.lean
  3063. rcases1.lean
  3064. readDir.lean
  3065. readDir.lean.out.expected
  3066. readerThe.lean
  3067. realPath.lean
  3068. realPath.lean.out.ignored
  3069. recCommonPrefixAlpha.lean
  3070. recconstructorcrash.lean
  3071. recInfo1.lean
  3072. recommendedSpelling.lean
  3073. reduce1.lean
  3074. reduce2.lean
  3075. reduce3.lean
  3076. reduce3.lean.out.expected
  3077. reduceArity.lean
  3078. reduceArity.lean.out.expected
  3079. reduceBEqSimproc.lean
  3080. reduceBool.lean
  3081. reduceBool.lean.out.expected
  3082. reduceCtorIdxSimproc.lean
  3083. reducibilityAttrValidation.lean
  3084. reducibleClassField_perf.lean
  3085. reductionBug.lean
  3086. redundantDeprecatedWarnings.lean
  3087. redundantVisibility.lean
  3088. ref1.lean
  3089. ref1.lean.out.expected
  3090. refl.lean
  3091. reflectiveIndPred.lean
  3092. reflectiveIndPred.lean.out.expected
  3093. Reformat.lean
  3094. Reformat.lean.input
  3095. Reformat.lean.out.expected
  3096. regressions3210.lean
  3097. Reid1.lean
  3098. Reid1.lean.out.expected
  3099. renameI.lean
  3100. renameI.lean.out.expected
  3101. renameI2.lean
  3102. renameI2.lean.out.expected
  3103. renameSelf.lean
  3104. renaming.lean
  3105. repeat.lean
  3106. repeatConv.lean
  3107. replace.lean
  3108. replace.lean.out.expected
  3109. replace_tac.lean
  3110. replayConst.lean
  3111. repr.lean
  3112. repr.lean.out.expected
  3113. repr_empty.lean
  3114. repr_issue.lean
  3115. repr_issue.lean.out.expected
  3116. reprove.lean
  3117. reserved.lean
  3118. reservedNameResolution.lean
  3119. resolveGlobalName.lean
  3120. resolveGlobalName.lean.out.expected
  3121. resolveLVal.lean
  3122. returnOptIssue.lean
  3123. revert1.lean
  3124. revertlet.lean
  3125. revertlet.lean.out.expected
  3126. revertMetavarKind.lean
  3127. rewrite.lean
  3128. rewrites.lean
  3129. rfl_simp_thm.lean
  3130. rfl_simp_thm.lean.out.expected
  3131. rflApplyFoApprox.lean
  3132. rflApplyFoApprox.lean.out.expected
  3133. rflProofsCongrCastsIssue.lean
  3134. rflReducibility.lean
  3135. rflTacticErrors.lean
  3136. robinson.lean
  3137. robinson.lean.out.expected
  3138. root.lean
  3139. root.lean.out.expected
  3140. rossel1.lean
  3141. rossel1.lean.out.expected
  3142. run_cmd.lean
  3143. run_meta1.lean
  3144. run_test.sh
  3145. runSTBug.lean
  3146. runSTBug.lean.out.expected
  3147. rw_inst_implicit_args.lean
  3148. rw_inst_mvars.lean
  3149. rwEqThms.lean
  3150. rwEqThms.lean.out.expected
  3151. rwPrioritizesLCtxOverEnv.lean
  3152. rwRegression.lean
  3153. rwWithElabError.lean
  3154. safeExp.lean
  3155. safeShadowing.lean
  3156. sanitizeMacroScopes.lean
  3157. sanitizeMacroScopes.lean.out.expected
  3158. sarray.lean
  3159. sarray.lean.out.ignored
  3160. scc.lean
  3161. scopeCacheProofs.lean
  3162. scopedCommandAfterOpen.lean
  3163. scopedCommandAfterOpen.lean.out.expected
  3164. scopedHindingIssue.lean
  3165. scopedHindingIssue.lean.out.expected
  3166. scopedLocalReducibility.lean
  3167. scopedParsers.lean
  3168. scopedParsers.lean.out.expected
  3169. scopedParsers2.lean
  3170. scopedParsers2.lean.out.expected
  3171. scopedunifhint.lean
  3172. scopedunifhint.lean.out.expected
  3173. sealCommand.lean
  3174. secVarBug.lean
  3175. secVarBug.lean.out.expected
  3176. sepByIndentQuot.lean
  3177. sepByIndentQuot.lean.out.expected
  3178. seqToCodeIssue.lean
  3179. seqToCodeIssue.lean.out.expected
  3180. set.lean
  3181. set_lit_unexpand.lean
  3182. setOptionErrors.lean
  3183. setOptionTermTactic.lean
  3184. setOptionTermTactic.lean.out.expected
  3185. setStructInstNotation.lean
  3186. seval1.lean
  3187. sharecommon.lean
  3188. sharecommon_mpz.lean
  3189. show_term.lean
  3190. showTactic.lean
  3191. showTests.lean
  3192. shrinkFn.lean
  3193. sigmaprec.lean
  3194. sign.lean
  3195. simp-elab-recover.lean
  3196. simp1.lean
  3197. simp1.lean.out.ignored
  3198. simp2.lean
  3199. simp3.lean
  3200. simp4.lean
  3201. simp5.lean
  3202. simp6.lean
  3203. simp_all.lean
  3204. simp_all_contextual.lean
  3205. simp_all_duplicateHyps.lean
  3206. simp_all_duplicateHyps.lean.out.expected
  3207. simp_arith_deprecated.lean
  3208. simp_arith_issues.lean
  3209. simp_arith_issues.lean.out.expected
  3210. simp_cache_perf_issue.lean
  3211. simp_cache_perf_issue.lean.out.expected
  3212. simp_cases.lean
  3213. simp_dsimp.lean
  3214. simp_dsimp.lean.out.expected
  3215. simp_eqn_bug.lean
  3216. simp_failIfUnchanged.lean
  3217. simp_inst_implict_args.lean
  3218. simp_int_arith.lean
  3219. simp_locals.lean
  3220. simp_locals_module.lean
  3221. simp_nat_arith.lean
  3222. simp_proj_transparency_issue.lean
  3223. simp_reducibleClassField.lean
  3224. simp_rfl_check_transparency.lean
  3225. simp_suggestions.lean
  3226. simp_trace_backtrack.lean
  3227. simp_trace_backtrack.lean.out.expected
  3228. simpa_reducible.lean
  3229. simpArith1.lean
  3230. simpArith1.lean.out.expected
  3231. simpArithCacheIssue.lean
  3232. simpArrayIdx.lean
  3233. simpAtDefIssue.lean
  3234. simpAutoUnfold.lean
  3235. simpBool.lean
  3236. simpBug.lean
  3237. simpCacheTest.lean
  3238. simpCasesOnCtorBug.lean
  3239. simpCasesOnCtorBug.lean.out.ignored
  3240. simpcfg.lean
  3241. simpcfg.lean.out.expected
  3242. simpCnstr1.lean
  3243. simpCondLemma.lean
  3244. simpConfigPropagationIssue1.lean
  3245. simpConfigPropagationIssue3.lean
  3246. simpDecide.lean
  3247. simpDefToUnfold.lean
  3248. simpDiag.lean
  3249. simpDiag.lean.out.expected
  3250. simpDisch.lean
  3251. simpDisch.lean.out.expected
  3252. simpDischargeLoop.lean
  3253. simpDischargeLoop.lean.out.expected
  3254. simpExtraArgsBug.lean
  3255. simpExtraArgsBug.lean.out.expected
  3256. simpGround1.lean
  3257. simpGround1.lean.out.expected
  3258. simpHave.lean
  3259. simpHigherOrder.lean
  3260. simpIfPre.lean
  3261. simpImpLocal.lean
  3262. simpIndexDiag.lean
  3263. simpIndexDiag.lean.out.expected
  3264. simpInv.lean
  3265. simpIssue.lean
  3266. simpJpCasesDepBug.lean
  3267. simple_ground_extraction.lean
  3268. simple_reuse.lean
  3269. simpLetFunIssue.lean
  3270. simpLoopBug.lean
  3271. simpLoopProtection.lean
  3272. simpMatch.lean
  3273. simpMatchDiscr.lean
  3274. simpMatchDiscr.lean.out.expected
  3275. simpMatchDiscrIssue.lean
  3276. simpMatchEta.lean
  3277. simpOnly.lean
  3278. simpPartialApp.lean
  3279. simpPartialApp.lean.out.expected
  3280. simpPrefixIssue.lean
  3281. simpPrefixIssue.lean.out.expected
  3282. simpPreIssue.lean
  3283. simpPreprocess.lean
  3284. simpPreprocess.lean.out.expected
  3285. simpPrio.lean
  3286. simproc1.lean
  3287. simproc2.lean
  3288. simproc_builtin_erase.lean
  3289. simproc_disable_issue.lean
  3290. simproc_disable_issue.lean.out.expected
  3291. simproc_erase.lean
  3292. simproc_panic.lean
  3293. simproc_timeout.lean
  3294. simproc_timeout.lean.out.expected
  3295. simprocChar.lean
  3296. simprocChar.lean.out.expected
  3297. simprocDigitChar.lean
  3298. simprocEval1.lean
  3299. simprocEval1.lean.out.expected
  3300. simprocEval2.lean
  3301. simprocEval2.lean.out.expected
  3302. simprocEval3.lean
  3303. simprocEval3.lean.out.expected
  3304. simprocEval4.lean
  3305. simprocEval4.lean.out.expected
  3306. simprocFin.lean
  3307. simprocNat.lean
  3308. simprocSInt.lean
  3309. simprocString.lean
  3310. simprocTrace.lean
  3311. simprocTrace.lean.out.expected
  3312. simprocUInt.lean
  3313. simpRwBug.lean
  3314. simpSInt.lean
  3315. simpStar.lean
  3316. simpStarHyp.lean
  3317. simpTrace.lean
  3318. simpTracePostIssue.lean
  3319. simpTracePostIssue.lean.out.expected
  3320. simpUnfoldAbbrev.lean
  3321. simpUnusedArgs.lean
  3322. simpVarHead.lean
  3323. simpZetaFalse.lean
  3324. simpZetaFalse.lean.out.expected
  3325. sint-abs.lean
  3326. sint_basic.lean
  3327. sint_basic.lean.out.expected
  3328. sint_conversions.lean
  3329. sint_div_overflow.lean
  3330. sint_div_overflow.lean.out.expected
  3331. sizeof.lean
  3332. sizeof.lean.out.expected
  3333. sizeof1.lean
  3334. sizeof1.lean.out.expected
  3335. sizeof2.lean
  3336. sizeof2.lean.out.expected
  3337. sizeof3.lean
  3338. sizeof3.lean.out.expected
  3339. sizeof4.lean
  3340. sizeof4.lean.out.expected
  3341. sizeof5.lean
  3342. sizeof5.lean.out.expected
  3343. sizeof6.lean
  3344. sizeof6.lean.out.expected
  3345. skipAssignedInstances.lean
  3346. skipKernelTC.lean
  3347. slice.lean
  3348. smartUnfolding.lean
  3349. smartUnfolding.lean.out.expected
  3350. smartUnfoldingBug.lean
  3351. smartUnfoldingMatch.lean
  3352. smartUnfoldingMatch.lean.out.expected
  3353. snapshotTree.lean
  3354. snapshotTree.lean.out.expected
  3355. solve_by_elim.lean
  3356. solve_by_elim_suggestions.lean
  3357. som1.lean
  3358. sorry.lean
  3359. sorryWarning.lean
  3360. sorryWarning.lean.out.expected
  3361. sparseCasesOn.lean
  3362. spec_issue.lean
  3363. spec_issue.lean.out.expected
  3364. spec_limit.lean
  3365. specbug.lean
  3366. specFixedHOParamModuloErased.lean
  3367. specialize1.lean
  3368. specialize2.lean
  3369. specialize3.lean
  3370. specialize_cache_miscompile.lean
  3371. specInvariantAttr.lean
  3372. split1.lean
  3373. split2.lean
  3374. split3.lean
  3375. split_mvars_target.lean
  3376. splitAtCode.lean
  3377. splitErrors.lean
  3378. splitIfIssue.lean
  3379. splitIfIssue.lean.out.expected
  3380. splitImplicitReducible.lean
  3381. splitIssue.lean
  3382. splitIssue.lean.out.expected
  3383. splitIssue2.lean
  3384. splitIssue2.lean.out.expected
  3385. splitIssue3.lean
  3386. splitIssue3.lean.out.expected
  3387. splitList.lean
  3388. splitList.lean.out.expected
  3389. splitOrderIssue.lean
  3390. spredNotation.lean
  3391. spredProofMode.lean
  3392. st_test.lean
  3393. starsAndBars.lean
  3394. state12.lean
  3395. state8.lean
  3396. stateRef.lean
  3397. stdDoPostUnit.lean
  3398. stdio.lean
  3399. stdio.lean.before.sh
  3400. stdio.lean.out.expected
  3401. stream.lean
  3402. stream.lean.out.expected
  3403. streamEqIssue.lean
  3404. streamEqIssue.lean.out.expected
  3405. strictImplicit.lean
  3406. strictImplicit.lean.out.expected
  3407. string.lean
  3408. string_cases.lean
  3409. string_cases.lean.out.expected
  3410. string_gaps.lean
  3411. string_imp.lean
  3412. string_imp.lean.out.expected
  3413. string_imp2.lean
  3414. string_imp2.lean.out.expected
  3415. string_kmp.lean
  3416. string_neq_kernel_cost.lean
  3417. string_pos_grind.lean
  3418. string_replace.lean
  3419. string_simprocs.lean
  3420. string_slice.lean
  3421. string_termination.lean
  3422. string_toNat_underscores.lean
  3423. strInterpolation.lean
  3424. strInterpolation.lean.out.expected
  3425. strLitProj.lean
  3426. strLitProj.lean.out.expected
  3427. struct1.lean
  3428. struct1.lean.out.expected
  3429. struct2.lean
  3430. struct2.lean.out.expected
  3431. struct3.lean
  3432. struct_inst_typed.lean
  3433. struct_instance_in_eqn.lean
  3434. structBinderIdent.lean
  3435. structBinderUpdates.lean
  3436. structEqns.lean
  3437. structInst.lean
  3438. structInst2.lean
  3439. structInst3.lean
  3440. structInst4.lean
  3441. structInstExtraEta.lean
  3442. structInstFast.lean
  3443. structInstSourcesLeftToRight.lean
  3444. structInstSourcesLeftToRight.lean.out.expected
  3445. structInstUpdates.lean
  3446. structNamedParentProj.lean
  3447. structNoBody.lean
  3448. structPrivateFieldBug.lean
  3449. structPrivateFieldBug2.lean
  3450. structuralEqn6.lean
  3451. structuralEqns.lean
  3452. structuralEqns.lean.out.expected
  3453. structuralEqns2.lean
  3454. structuralEqns2.lean.out.expected
  3455. structuralEqns3.lean
  3456. structuralEqns3.lean.out.expected
  3457. structuralEqns4.lean
  3458. structuralEqns5.lean
  3459. structuralIssue.lean
  3460. structuralIssue2.lean
  3461. structuralMutual.lean
  3462. structuralNamedF.lean
  3463. structuralOverNested.lean
  3464. structuralRec1.lean
  3465. structuralRec2.lean
  3466. structure.lean
  3467. structure_recursive.lean
  3468. structureElab.lean
  3469. structWithAlgTCSynth.lean
  3470. structWithAlgTCSynth.lean.out.expected
  3471. stuckMVarBug.lean
  3472. stuckMVarBug.lean.out.expected
  3473. stuckTC.lean
  3474. stxKindInsideNamespace.lean
  3475. stxKindInsideNamespace.lean.out.expected
  3476. stxMacro.lean
  3477. stxMacro.lean.out.expected
  3478. subarray_split.lean
  3479. subexpr.lean
  3480. subscript_parser.lean
  3481. subset.lean
  3482. subset.lean.out.expected
  3483. subsingletonCasesOn.lean
  3484. subst.lean
  3485. subst1.lean
  3486. subst1.lean.out.ignored
  3487. substlet.lean
  3488. substVars.lean
  3489. substWithoutExpectedType.lean
  3490. subtype_inj.lean
  3491. suffices.lean
  3492. sym_apply_bug.lean
  3493. sym_arith_classify.lean
  3494. sym_arith_reify.lean
  3495. sym_cbv.lean
  3496. sym_cbv_12336.lean
  3497. sym_congrInfo.lean
  3498. sym_discrtree_eta.lean
  3499. sym_dsimp.lean
  3500. sym_dsimp_1.lean
  3501. sym_dsimp_2.lean
  3502. sym_dsimp_bug.lean
  3503. sym_dsimp_match.lean
  3504. sym_eta_mwe.lean
  3505. sym_getMaxFVar.lean
  3506. sym_instantiate.lean
  3507. sym_interactive1.lean
  3508. sym_interactive_bugs.lean
  3509. sym_intro.lean
  3510. sym_intro_have.lean
  3511. sym_intro_issue.lean
  3512. sym_issue_13416.lean
  3513. sym_liftLower.lean
  3514. sym_pattern.lean
  3515. sym_pattern_2.lean
  3516. sym_pattern_3.lean
  3517. sym_pattern_level.lean
  3518. sym_pattern_universe_issue.lean
  3519. sym_proj_issue.lean
  3520. sym_register_variant1.lean
  3521. sym_simp_1.lean
  3522. sym_simp_2.lean
  3523. sym_simp_3.lean
  3524. sym_simp_4.lean
  3525. sym_simp_5.lean
  3526. sym_simp_adapt1.lean
  3527. sym_simp_cd.lean
  3528. sym_simp_cd_unit.lean
  3529. sym_simp_dsl_control1.lean
  3530. sym_simp_interactive1.lean
  3531. sym_simp_perm1.lean
  3532. sym_simp_set.lean
  3533. sym_simproc_dsl1.lean
  3534. symbolFrequency.lean
  3535. symbolFrequency_foldRelevantConsts.lean
  3536. symm.lean
  3537. sync_barrier.lean
  3538. sync_channel.lean
  3539. sync_mutex.lean
  3540. sync_notify.lean
  3541. sync_recursive_mutex.lean
  3542. sync_shared_mutex.lean
  3543. syntax1.lean
  3544. syntax1.lean.out.expected
  3545. syntaxAbbrevQuot.lean
  3546. syntaxAbbrevQuot.lean.out.expected
  3547. syntaxInNamespacesAndPP.lean
  3548. syntaxInNamespacesAndPP.lean.out.expected
  3549. syntaxPrio.lean
  3550. syntaxPrio.lean.out.expected
  3551. synth1.lean
  3552. synth1.lean.out.expected
  3553. syntheticOpaqueReadOnly.lean
  3554. syntheticOpaqueReadOnly.lean.out.expected
  3555. synthInstsIssue.lean
  3556. synthInstsIssue.lean.out.expected
  3557. synthOrderRegression.lean
  3558. synthOrderRegression.lean.out.expected
  3559. synthPending1.lean
  3560. synthPendingBug.lean
  3561. tabulate.lean
  3562. tabulate.lean.out.expected
  3563. tactic.lean
  3564. tactic1.lean
  3565. tactic1.lean.out.expected
  3566. tactic_config.lean
  3567. tacticDoc.lean
  3568. tacticDocAllModule.lean
  3569. tacticDocAllNonmod.lean
  3570. tacticDocUserName.lean
  3571. tacticExtOverlap.lean
  3572. tacticTests.lean
  3573. tagged_return_1.lean
  3574. tagged_return_2.lean
  3575. takeSimpEqns.lean
  3576. task_iterators.lean
  3577. task_test.lean
  3578. task_test.lean.out.ignored
  3579. task_test2.lean
  3580. task_test2.lean.out.ignored
  3581. task_test_io.lean
  3582. task_test_io.lean.out.expected
  3583. taskState.lean
  3584. tc_cache.lean
  3585. tc_eta_struct_issue.lean
  3586. tc_eta_struct_issue.lean.out.expected
  3587. tcUnivIssue.lean
  3588. tempfile.lean
  3589. termElab.lean
  3590. terminalAsSorry.lean
  3591. terminalAsSorry.lean.out.expected
  3592. termination_by_where.lean
  3593. terminationByStructurally.lean
  3594. termParserAttr.lean
  3595. TermSeq.lean
  3596. test_binary_dec_proc_fold.lean
  3597. test_proj_hints.lean
  3598. test_simp_reducible_class.lean
  3599. thmIsProp.lean
  3600. thmsOpaque.lean
  3601. thunk.lean
  3602. thunk.lean.out.expected
  3603. thunkTaskCasesOn.lean
  3604. time.lean
  3605. timeAPI.lean
  3606. timeCanonFormats.lean
  3607. timeClassOperations.lean
  3608. timeFormats.lean
  3609. timeIO.lean
  3610. timeLimits.lean
  3611. timeLocalDateTime.lean
  3612. timeNegative.lean
  3613. timeOperations.lean
  3614. timeOperationsOffset.lean
  3615. timeParse.lean
  3616. timeSet.lean
  3617. timeSub.lean
  3618. timeTzifParse.lean
  3619. to_array_csimp.lean
  3620. toArrayEq.lean
  3621. toDeclEtaBug.lean
  3622. toExpr.lean
  3623. toExpr.lean.out.expected
  3624. toExpr2.lean
  3625. toExpr2.lean.out.expected
  3626. toFieldNameIssue.lean
  3627. toFieldNameIssue.lean.out.expected
  3628. toFromJson.lean
  3629. tojson_fromjson_perf_issue.lean
  3630. toLCNFCacheBug.lean
  3631. toLCNFCacheBug.lean.out.ignored
  3632. trace.lean
  3633. trace_synth.lean
  3634. traceClassScopes.lean
  3635. traceClassScopes.lean.out.expected
  3636. traceElabIssue.lean
  3637. traceFormat.lean
  3638. traceStateBacktracking.lean
  3639. traceStateBacktracking.lean.out.expected
  3640. traceTacticSteps.lean
  3641. traceTacticSteps.lean.out.expected
  3642. trackZetaDeltaCacheIssue.lean
  3643. trans.lean
  3644. trans.lean.out.expected
  3645. treeMap.lean
  3646. treeMap2.lean
  3647. treeNode.lean
  3648. trivial_uint.lean
  3649. try_eval_suggest.lean
  3650. try_first_par.lean
  3651. try_heartbeats.lean
  3652. try_induction.lean
  3653. try_library_suggestions.lean
  3654. try_panic.lean
  3655. try_parallelism.lean
  3656. try_prelude.lean
  3657. try_register_builtin.lean
  3658. try_solve_by_elim.lean
  3659. try_solve_by_elim.lean.out.expected
  3660. try_user_suggestions.lean
  3661. tryHeuristicPerfIssue.lean
  3662. tryHeuristicPerfIssue.lean.out.expected
  3663. tryHeuristicPerfIssue2.lean
  3664. tryHeuristicPerfIssue2.lean.out.expected
  3665. tryOnEmptyBy.lean
  3666. tryPostponeIssue.lean
  3667. type_as_hole.lean
  3668. type_class_performance1.lean
  3669. type_class_performance1.lean.out.expected
  3670. typeAscImp.lean
  3671. typeCheckNote.lean
  3672. typeclass_append.lean
  3673. typeclass_append.lean.out.expected
  3674. typeclass_coerce.lean
  3675. typeclass_coerce.lean.out.expected
  3676. typeclass_diamond.lean
  3677. typeclass_easy.lean
  3678. typeclass_easy.lean.out.expected
  3679. typeclass_loop.lean
  3680. typeclass_metas_internal_goals1.lean
  3681. typeclass_metas_internal_goals2.lean
  3682. typeclass_metas_internal_goals3.lean
  3683. typeclass_metas_internal_goals4.lean
  3684. typeclass_outparam.lean
  3685. typeOccursCheckIssue.lean
  3686. ubscalar.lean
  3687. ubscalar.lean.out.ignored
  3688. ugetBorrowed.lean
  3689. uintCtors.lean
  3690. uintCtors.lean.out.expected
  3691. uintMatch.lean
  3692. uintMatch.lean.out.expected
  3693. unboxStruct.lean
  3694. unboxStruct.lean.out.expected
  3695. unexpander.lean
  3696. unexpander.lean.out.expected
  3697. unexpandersNamespaces.lean
  3698. unexpandersNamespaces.lean.out.expected
  3699. UnexpandSubtype.lean
  3700. UnexpandSubtype.lean.out.expected
  3701. unexpected_result_with_bind.lean
  3702. unfold1.lean
  3703. unfold1.lean.out.expected
  3704. unfold_reducible_class_proj.lean
  3705. unfoldDefEq.lean
  3706. unfoldDefEq.lean.out.expected
  3707. unfoldLemma.lean
  3708. unfoldMany.lean
  3709. unfoldPartialRegression.lean
  3710. unfoldr.lean
  3711. unfoldReduceMatch.lean
  3712. unfoldReduceMatch.lean.out.expected
  3713. unfoldTactic.lean
  3714. unhygienic.lean
  3715. unhygienic.lean.out.expected
  3716. unhygienicCode.lean
  3717. unhygienicCode.lean.out.expected
  3718. unif_issue.lean
  3719. unif_issue.lean.out.expected
  3720. unif_issue2.lean
  3721. unif_issue2.lean.out.expected
  3722. unifhint1.lean
  3723. unifhint2.lean
  3724. unifhint3.lean
  3725. unifHintAndTC.lean
  3726. unifHintAndTC.lean.out.expected
  3727. unihint.lean
  3728. unihint.lean.out.expected
  3729. univ_out_params.lean
  3730. univCnstrApprox.lean
  3731. univCnstrApprox.lean.out.expected
  3732. univIssue.lean
  3733. univParamIssue.lean
  3734. univPolyEnum.lean
  3735. unlock_limits.lean
  3736. unnecessaryUnfolding.lean
  3737. unnecessaryUnfolding.lean.out.expected
  3738. unsafeConst.lean
  3739. unsafeConst.lean.out.expected
  3740. unsafeInit.lean
  3741. unsafeTerm.lean
  3742. unusedLet.lean
  3743. unusedLet.lean.out.expected
  3744. unusedVarDoMatch.lean
  3745. unusedVarDoMWE.lean
  3746. unusedWarningAtStructUpdate.lean
  3747. update.lean
  3748. updateExprIssue.lean
  3749. updateExprIssue.lean.out.expected
  3750. updateLevelIssues.lean
  3751. updateLevelIssues.lean.out.expected
  3752. Uri.lean
  3753. Uri.lean.out.expected
  3754. usesOfNoncomputable.lean
  3755. utf8英語.lean
  3756. valueOfTerm.lean
  3757. varBinderUpdate.lean
  3758. variable.lean
  3759. vcgenDepAssertionLattice.lean
  3760. vcgenFrames.lean
  3761. vcgenMatchDependentDiscr.lean
  3762. vcgenSpecAbbrev.lean
  3763. vcgenSymBlock.lean
  3764. vcgenUntil.lean
  3765. versoDocClass.lean
  3766. versoDocCustomRenderer.lean
  3767. versoDocCustomRendererNonModule.lean
  3768. versoDocFirstLineHeader.lean
  3769. versoDocIndentedHeader.lean
  3770. versoDocMacroModeMismatch.lean
  3771. versoDocMarkdown.lean
  3772. versoDocMarkdownRendering.lean
  3773. versoDocMetadata.lean
  3774. versoDocModuleDeclOnly.lean
  3775. versoDocModuleFallback.lean
  3776. versoDocModuleGiven.lean
  3777. versoDocModuleVersoOnly.lean
  3778. versoDocNesting.lean
  3779. versoDocParseError.lean
  3780. versoDocs.lean
  3781. versoDocs.lean.out.expected
  3782. versoDocSetOptionIn.lean
  3783. versoDocsMacro.lean
  3784. versoDocsModule.lean
  3785. versoDocSuggestionNoImport.lean
  3786. versoDocsWhere.lean
  3787. versoDocWarningsErrors.lean
  3788. waitForExpectedType.lean
  3789. warnSorry.lean
  3790. weak_specialize.lean
  3791. wf_preprocess.lean
  3792. wf_preprocess_leak.lean
  3793. wfcomputable.lean
  3794. wfEqns1.lean
  3795. wfEqns1.lean.out.expected
  3796. wfEqns2.lean
  3797. wfEqns3.lean
  3798. wfEqns4.lean
  3799. wfEqns5.lean
  3800. wfEqnsIssue.lean
  3801. wfForIn.lean
  3802. wfirred.lean
  3803. wfLean3Issue.lean
  3804. wfOmega.lean
  3805. wfOverapplicationIssue.lean
  3806. wfrec-nat.lean
  3807. wfrecUnary.lean
  3808. wfrecUnusedLet.lean
  3809. wfrecUnusedLet.lean.out.expected
  3810. WFRelSearch.lean
  3811. wfSum.lean
  3812. wfUnfold.lean
  3813. wfWithSidecondition.lean
  3814. where1.lean
  3815. whereCmd.lean
  3816. whereCmdModule.lean
  3817. whereFinally.lean
  3818. while_extrinsic.lean
  3819. whileRepeat.lean
  3820. whnfDelayedMVarIssue.lean
  3821. whnfProj.lean
  3822. whnfProj.lean.out.expected
  3823. WindowsNewlines.lean
  3824. with_unfolding_none.lean
  3825. withAssignableSyntheticOpaqueBug.lean
  3826. withAssignableSyntheticOpaqueBug.lean.out.expected
  3827. withLocation.lean
  3828. withLocation.lean.out.expected
  3829. withReducibleAndInstancesCrash.lean
  3830. withReducibleAndInstancesCrash.lean.out.ignored
  3831. withSetOptionIn.lean
  3832. withWeakNamespace.lean
  3833. withWeakNamespace.lean.out.expected
  3834. workspaceSymbols.lean
  3835. workspaceSymbols.lean.out.expected
  3836. zeroExitPoints.lean
  3837. zeroExitPoints.lean.out.ignored
  3838. zetaDelta.lean
  3839. zetaDeltaFalseDefEqIssue.lean
  3840. zetaDeltaIssue.lean
  3841. zetaDeltaSet.lean
  3842. zetaDeltaSet.lean.out.expected
  3843. zetaDeltaTryThisIssue.lean
  3844. zetaDSimpIssue.lean
  3845. zetaUnused.lean
  3846. zipper.lean
  3847. zipper.lean.out.expected