Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/setConfig/./tests/lean/run
tree: e943389eaffcabff3c4b0fc4b65bea6c7538139e [search]
  1. .gitattributes
  2. .gitignore
  3. 1016.lean
  4. 1017.lean
  5. 1018.lean
  6. 1020.lean
  7. 1022.lean
  8. 1024.lean
  9. 1025.lean
  10. 1026.lean
  11. 1029.lean
  12. 102_lean3.lean
  13. 1030.lean
  14. 1037.lean
  15. 1051.lean
  16. 1058.lean
  17. 1074a.lean
  18. 108.lean
  19. 1080.lean
  20. 111.lean
  21. 1113b.lean
  22. 1118.lean
  23. 1120.lean
  24. 1123.lean
  25. 1124.lean
  26. 1127.lean
  27. 1132.lean
  28. 1143.lean
  29. 1155.lean
  30. 1156.lean
  31. 1158.lean
  32. 1163.lean
  33. 1168.lean
  34. 1169.lean
  35. 1171.lean
  36. 1179b.lean
  37. 1182.lean
  38. 1184.lean
  39. 1192.lean
  40. 1193a.lean
  41. 1193b.lean
  42. 1194.lean
  43. 1200.lean
  44. 1202.lean
  45. 121.lean
  46. 1224.lean
  47. 1228.lean
  48. 1230.lean
  49. 1234.lean
  50. 1236.lean
  51. 1237.lean
  52. 1247.lean
  53. 125.lean
  54. 1253.lean
  55. 1267.lean
  56. 1274.lean
  57. 1289.lean
  58. 1293.lean
  59. 1299.lean
  60. 1300.lean
  61. 1302.lean
  62. 1305.lean
  63. 1308.lean
  64. 1311.lean
  65. 1333.lean
  66. 1337.lean
  67. 1342.lean
  68. 1359.lean
  69. 1360.lean
  70. 1361.lean
  71. 1361b.lean
  72. 1365.lean
  73. 1372.lean
  74. 1373.lean
  75. 1374.lean
  76. 1375.lean
  77. 1380.lean
  78. 1385.lean
  79. 1389.lean
  80. 1408.lean
  81. 1411.lean
  82. 1419.lean
  83. 1420.lean
  84. 1426.lean
  85. 1435.lean
  86. 1436.lean
  87. 1441.lean
  88. 1547.lean
  89. 1549.lean
  90. 1558.lean
  91. 1575.lean
  92. 1615.lean
  93. 1650.lean
  94. 1674.lean
  95. 1679.lean
  96. 1684.lean
  97. 1686.lean
  98. 1692.lean
  99. 1697.lean
  100. 1711.lean
  101. 1725.lean
  102. 1730.lean
  103. 175.lean
  104. 1780.lean
  105. 1785.lean
  106. 1787.lean
  107. 1808.lean
  108. 1812.lean
  109. 1813.lean
  110. 1815.lean
  111. 1822.lean
  112. 1829.lean
  113. 1841.lean
  114. 1842.lean
  115. 1848.lean
  116. 1850.lean
  117. 1851.lean
  118. 1852.lean
  119. 1869.lean
  120. 1882.lean
  121. 1883.lean
  122. 1886.lean
  123. 1892.lean
  124. 1900.lean
  125. 1901.lean
  126. 1907.lean
  127. 1907orig.lean
  128. 1910.lean
  129. 1921.lean
  130. 1926.lean
  131. 1937.lean
  132. 1951.lean
  133. 1954.lean
  134. 1963.lean
  135. 1968.lean
  136. 1985.lean
  137. 1986.lean
  138. 2009.lean
  139. 2018.lean
  140. 2042.lean
  141. 2044.lean
  142. 2058.lean
  143. 2073.lean
  144. 2074.lean
  145. 2079.lean
  146. 2095.lean
  147. 2136.lean
  148. 2137.lean
  149. 2143.lean
  150. 2159.lean
  151. 2161.lean
  152. 2173.lean
  153. 2182.lean
  154. 2186.lean
  155. 2188.lean
  156. 2199.lean
  157. 2220.lean
  158. 2226.lean
  159. 2243.lean
  160. 2249.lean
  161. 2262.lean
  162. 2265.lean
  163. 2282.lean
  164. 2283.lean
  165. 229.lean
  166. 2291.lean
  167. 2299.lean
  168. 2311.lean
  169. 2344.lean
  170. 2389.lean
  171. 2461.lean
  172. 2500.lean
  173. 2552.lean
  174. 2558.lean
  175. 2575.lean
  176. 2615.lean
  177. 262.lean
  178. 2649.lean
  179. 2669.lean
  180. 2670.lean
  181. 2672.lean
  182. 269.lean
  183. 2690.lean
  184. 270.lean
  185. 2710.lean
  186. 2736.lean
  187. 28.lean
  188. 280.lean
  189. 281.lean
  190. 2810.lean
  191. 282.lean
  192. 2835.lean
  193. 2843.lean
  194. 2846.lean
  195. 2862.lean
  196. 2899.lean
  197. 29.lean
  198. 2901.lean
  199. 2905.lean
  200. 2914.lean
  201. 2916.lean
  202. 2939.lean
  203. 2942.lean
  204. 2966.lean
  205. 3022.lean
  206. 303.lean
  207. 3045.lean
  208. 305.lean
  209. 3079.lean
  210. 3091.lean
  211. 310.lean
  212. 3146.lean
  213. 3146.lean.expected.out
  214. 319.lean
  215. 3214.lean
  216. 3229.lean
  217. 3242.lean
  218. 3257.lean
  219. 326.lean
  220. 327.lean
  221. 329.lean
  222. 3313.lean
  223. 335.lean
  224. 337.lean
  225. 338.lean
  226. 3386.lean
  227. 3395.lean
  228. 34.lean
  229. 341.lean
  230. 343.lean
  231. 345.lean
  232. 3458_1.lean
  233. 3458_2.lean
  234. 3467.lean
  235. 3497.lean
  236. 3501.lean
  237. 3519.lean
  238. 3524.lean
  239. 3546.lean
  240. 3547.lean
  241. 3554.lean
  242. 3643.lean
  243. 3686.lean
  244. 3705.lean
  245. 3706.lean
  246. 3710.lean
  247. 3713.lean
  248. 3731.lean
  249. 3740.lean
  250. 3745.lean
  251. 3807.lean
  252. 382.lean
  253. 387.lean
  254. 3922.lean
  255. 394.lean
  256. 3943.lean
  257. 3965.lean
  258. 3965_2.lean
  259. 3965_3.lean
  260. 3996.lean
  261. 4051.lean
  262. 4064.lean
  263. 4086.lean
  264. 4101.lean
  265. 4144.lean
  266. 4171.lean
  267. 4203.lean
  268. 4213.lean
  269. 4219.lean
  270. 4230.lean
  271. 4251.lean
  272. 4290.lean
  273. 4306.lean
  274. 4310.lean
  275. 4313.lean
  276. 4318.lean
  277. 4320.lean
  278. 4334.lean
  279. 4339.lean
  280. 436.lean
  281. 4365.lean
  282. 436_lean3.lean
  283. 4381.lean
  284. 439.lean
  285. 4390.lean
  286. 4398.lean
  287. 4405.lean
  288. 4406.lean
  289. 441.lean
  290. 4413.lean
  291. 4462.lean
  292. 4465.lean
  293. 447_lean3.lean
  294. 452.lean
  295. 4534.lean
  296. 4547.lean
  297. 4555.lean
  298. 456.lean
  299. 4561.lean
  300. 457.lean
  301. 4573.lean
  302. 461a.lean
  303. 461b.lean
  304. 462.lean
  305. 463.lean
  306. 4636.lean
  307. 4644.lean
  308. 4662.lean
  309. 4670.lean
  310. 4673.lean
  311. 4677.lean
  312. 4686.lean
  313. 470_lean3.lean
  314. 471.lean
  315. 474_lean3.lean
  316. 4751.lean
  317. 4761.lean
  318. 4768.lean
  319. 4773.lean
  320. 481.lean
  321. 482.lean
  322. 4861.lean
  323. 4888.lean
  324. 492.lean
  325. 4920.lean
  326. 4928.lean
  327. 492_lean3.lean
  328. 4947.lean
  329. 498.lean
  330. 4983.lean
  331. 4985.lean
  332. 500_lean3.lean
  333. 501.lean
  334. 5046.lean
  335. 509.lean
  336. 5126.lean
  337. 5176.lean
  338. 5236.lean
  339. 52_lean3.lean
  340. 5333.lean
  341. 5359.lean
  342. 536.lean
  343. 5388.lean
  344. 5406.lean
  345. 5417.lean
  346. 5424.lean
  347. 5475.lean
  348. 5565.lean
  349. 561.lean
  350. 5634.lean
  351. 5664.lean
  352. 5668.lean
  353. 5672.lean
  354. 5674.lean
  355. 569.lean
  356. 5818.lean
  357. 5993.lean
  358. 602.lean
  359. 616.lean
  360. 633.lean
  361. 644.lean
  362. 646.lean
  363. 654.lean
  364. 664.lean
  365. 677.lean
  366. 696.lean
  367. 716.lean
  368. 753.lean
  369. 760.lean
  370. 764.lean
  371. 783.lean
  372. 788.lean
  373. 790.lean
  374. 793.lean
  375. 796.lean
  376. 815.lean
  377. 821.lean
  378. 837.lean
  379. 847.lean
  380. 854.lean
  381. 860.lean
  382. 879.lean
  383. 891.lean
  384. 909.lean
  385. 91_lean3.lean
  386. 944.lean
  387. 945.lean
  388. 946.lean
  389. 955.lean
  390. 968.lean
  391. 972.lean
  392. 974.lean
  393. 983.lean
  394. 986.lean
  395. 988.lean
  396. 998.lean
  397. 998Export.lean
  398. abstractExpr.lean
  399. ac_expr.lean
  400. ac_rfl.lean
  401. ack.lean
  402. ACltBug.lean
  403. adam1.lean
  404. adamTC.lean
  405. adamTC2.lean
  406. add_suggestion.lean
  407. addDecorationsWithoutPartial.lean
  408. addPPExplicitToExposeDiff.lean
  409. aig_optimizations.lean
  410. aig_shared.lean
  411. aig_stress.lean
  412. alex1.lean
  413. alg.lean
  414. alias.lean
  415. allGoals.lean
  416. and_intros.lean
  417. andCasesOnBug.lean
  418. anonymous_ctor_error_msg.lean
  419. anonymousCtor.lean
  420. appFinalizeIssue.lean
  421. appIssue.lean
  422. apply_tac.lean
  423. applytransp.lean
  424. approxDepth.lean
  425. array1.lean
  426. array_isEqvAux.lean
  427. array_simp.lean
  428. arrowDot.lean
  429. arthur1.lean
  430. arthur2.lean
  431. assertAfterBug.lean
  432. aStructPerfIssue.lean
  433. attachJp.lean
  434. autoboundIssues.lean
  435. autoLift.lean
  436. autoLiftIssue.lean
  437. autoparam.lean
  438. backtrackable_estate.lean
  439. balg.lean
  440. bigctor.lean
  441. bigmul.lean
  442. bigop.lean
  443. bindCasesIssue.lean
  444. binderNotation.lean
  445. binop.lean
  446. binop_binrel_perf_issue.lean
  447. binrec.lean
  448. binrel.lean
  449. binrelmacros.lean
  450. bitvec.lean
  451. bitvec_fin_literal_norm.lean
  452. bitvec_simproc.lean
  453. borrowBug.lean
  454. bubble.lean
  455. bugNatLitDiscrTree.lean
  456. bv_arith.lean
  457. bv_axiom_check.lean
  458. bv_bitblast_stress.lean
  459. bv_bitwise.lean
  460. bv_cast.lean
  461. bv_counterexample.lean
  462. bv_decide_bool.lean
  463. bv_decide_nat.lean
  464. bv_decide_rewriter.lean
  465. bv_errors.lean
  466. bv_extract.lean
  467. bv_inequality.lean
  468. bv_llvm.lean
  469. bv_math_lit_perf.lean
  470. bv_popcount.lean
  471. bv_reflection_stress.lean
  472. bv_shift.lean
  473. bv_substructure.lean
  474. bv_uninterpreted.lean
  475. bv_unused.lean
  476. bv_will_overflow.lean
  477. by_cases.lean
  478. byAsSorry.lean
  479. byteSliceIssue.lean
  480. calc.lean
  481. calcBug.lean
  482. calcInType.lean
  483. casePrime.lean
  484. casesAnyTypeIssue.lean
  485. casesRec.lean
  486. casesUsing.lean
  487. caseTacInMacros.lean
  488. catchThe.lean
  489. cdotAtSimpArg.lean
  490. cdotTests.lean
  491. change.lean
  492. change_tac.lean
  493. check.lean
  494. check_failure.lean
  495. checkAssignmentIssue.lean
  496. choiceExpectedTypeBug.lean
  497. choiceMacroRules.lean
  498. class_inductive.lean
  499. classAbbrev.lean
  500. classical.lean
  501. cleanup_forallTelescope.lean
  502. closure1.lean
  503. codeBindUnreachIssue.lean
  504. coeIssue1.lean
  505. coeIssue2.lean
  506. coeIssue3.lean
  507. coeIssues4.lean
  508. coelambda.lean
  509. CoeNew.lean
  510. coeOutParamIssue.lean
  511. coeOutParamIssue2.lean
  512. coeSort1.lean
  513. coeSort2.lean
  514. combinatorsAndWF.lean
  515. CommandExtOverlap.lean
  516. compatibleTypesBugAtLCNF.lean
  517. compatibleTypesEtaIssue.lean
  518. compiler_erase_bug.lean
  519. compiler_proj_bug.lean
  520. CompilerCSE.lean
  521. CompilerFindJoinPoints.lean
  522. CompilerFloatLetIn.lean
  523. CompilerProbe.lean
  524. CompilerPullInstances.lean
  525. CompilerSimp.lean
  526. compilerTest1.lean
  527. computedFields.lean
  528. concatElim.lean
  529. congrTactic.lean
  530. congrThm.lean
  531. congrThm2.lean
  532. constantCompilerBug.lean
  533. constFun.lean
  534. constFun2.lean
  535. constProp.lean
  536. constructor_as_variable.lean
  537. contra.lean
  538. contradiction1.lean
  539. contradictionExfalso.lean
  540. contradictionLoop.lean
  541. conv1.lean
  542. conv2.lean
  543. conv_arg.lean
  544. convcalc.lean
  545. core.lean
  546. crashDiv0.lean
  547. crlfToLf.lean
  548. csimp_type_error.lean
  549. csimpAttrFn.lean
  550. ctorAutoParams.lean
  551. currentDir.lean
  552. customEliminators.lean
  553. Daniel1.lean
  554. deBruijn.lean
  555. decAuxBug.lean
  556. decClassical.lean
  557. decEq.lean
  558. decidability_timeout.lean
  559. decideBang.lean
  560. decidelet.lean
  561. decideNative.lean
  562. decideTactic.lean
  563. declareConfigElabBug.lean
  564. declareConfigElabIssue.lean
  565. decreasingTacticUpdatedEnvIssue.lean
  566. deep1.lean
  567. def1.lean
  568. def10.lean
  569. def11.lean
  570. def12.lean
  571. def13.lean
  572. def14.lean
  573. def15.lean
  574. def16.lean
  575. def17.lean
  576. def18.lean
  577. def19.lean
  578. def2.lean
  579. def20.lean
  580. def3.lean
  581. def4.lean
  582. def5.lean
  583. def6.lean
  584. def7.lean
  585. def8.lean
  586. def9.lean
  587. defaultEliminator.lean
  588. defaultInstBacktrackIssue.lean
  589. defaulValueParamIssue.lean
  590. DefEqAssignBug.lean
  591. defEqVsWhnfI.lean
  592. delabApp.lean
  593. delabMatch.lean
  594. delabName.lean
  595. delabProjectionApp.lean
  596. delabStructInst.lean
  597. depElim1.lean
  598. depFieldIssue.lean
  599. depHd.lean
  600. deq.lean
  601. deriv.lean
  602. derivingBEq.lean
  603. derivingHashable.lean
  604. derivingInhabited.lean
  605. derivingNonempty.lean
  606. derivingRepr.lean
  607. diagnostics.lean
  608. diagnosticsMsgOptional.lean
  609. diagRec.lean
  610. diamond1.lean
  611. diamond2.lean
  612. diamond3.lean
  613. diamond4.lean
  614. diamond5.lean
  615. diff.lean
  616. discrRefinement.lean
  617. discrRefinement2.lean
  618. discrRefinement3.lean
  619. discrTreeKey.lean
  620. discrTreeOffset.lean
  621. discrTreeSimp.lean
  622. do_eqv.lean
  623. do_eqv_proofs.lean
  624. doElemAsTermNotation.lean
  625. dofun_prec.lean
  626. doLetElse.lean
  627. dollarProjIssue.lean
  628. doNotation1.lean
  629. doNotation2.lean
  630. doNotation3.lean
  631. doNotation4.lean
  632. doNotation5.lean
  633. doNotation6.lean
  634. Dorais1.lean
  635. dotNameIssue.lean
  636. dotNotationAndDefaultInstance.lean
  637. dotNotationRecDecl.lean
  638. doTrailingAtEOI.lean
  639. dottedCtorNamedArgPattern.lean
  640. dottedNameBug.lean
  641. dsimp1.lean
  642. dsimp2.lean
  643. dsimp_bv_simproc.lean
  644. dsimpNatLitIssue.lean
  645. dsimproc.lean
  646. DVec.lean
  647. dynamic.lean
  648. eagerInliningIssue.lean
  649. elab_cmd.lean
  650. elabAsElim.lean
  651. elabCmd.lean
  652. elabIte.lean
  653. eliminatorImplicitTargets.lean
  654. elimOptParam.lean
  655. elseCaseArrow.lean
  656. elseIfConfusion.lean
  657. emptycOverloadIssues.lean
  658. emptyLcnf.lean
  659. enumDecEq.lean
  660. enumNoConfusionIssue.lean
  661. eq_some_iff_get_eq_issue.lean
  662. eqndrecEtaLCNFIssue.lean
  663. eqnOptions.lean
  664. eqnsAtSimp.lean
  665. eqnsAtSimp2.lean
  666. eqnsAtSimp3.lean
  667. eqnsPrio.lean
  668. eqnsProjections.lean
  669. eqnsReducible.lean
  670. eqTheoremForVec.lean
  671. eqThm.lean
  672. eqThmWithMoreThanOneAsPattern.lean
  673. eqValue.lean
  674. erased.lean
  675. eraseReps.lean
  676. eraseSuffix.lean
  677. erasureConfusion.lean
  678. etaFirst.lean
  679. etaStruct.lean
  680. etaStructProofIrrelIssue.lean
  681. eval.lean
  682. eval_unboxed_const.lean
  683. evalBuiltinInit.lean
  684. evalconst.lean
  685. evalDo.lean
  686. evalInit.lean
  687. evalProp.lean
  688. evalTacticBug.lean
  689. exfalsoBug.lean
  690. exists.lean
  691. exp.lean
  692. expandAbbrevAtIsClass.lean
  693. expandWhereStructInstIssue.lean
  694. expectedTypePropagation.lean
  695. explicitApp.lean
  696. explicitMotive.lean
  697. explictOpenDeclIssue.lean
  698. expr1.lean
  699. expr_maps.lean
  700. ExprLens.lean
  701. ext.lean
  702. ext1.lean
  703. extensibleTacticBug.lean
  704. extern.lean
  705. extmacro.lean
  706. false_or_by_contra.lean
  707. falseElimAtSimpLocalDecl.lean
  708. fieldAbbrevInPat.lean
  709. fieldAutoBound.lean
  710. fieldDefaultValueWithoutType.lean
  711. fieldIssue.lean
  712. fieldNamesWithMinus.lean
  713. fieldTypeBug.lean
  714. filter.lean
  715. fin_two_pow.lean
  716. finally.lean
  717. finDotCtor.lean
  718. finLit.lean
  719. finMatch.lean
  720. flat_expr.lean
  721. float1.lean
  722. float_cases_bug.lean
  723. float_from_bignum.lean
  724. floatarray.lean
  725. floatOptParam.lean
  726. foApprox.lean
  727. foldConsts.lean
  728. foldLits.lean
  729. forBodyResultTypeIssue.lean
  730. forInElabBug.lean
  731. forInPArray.lean
  732. forInRangeWF.lean
  733. forInReturnPropagation.lean
  734. forInUniv.lean
  735. formatterTokenTable.lean
  736. forOutParamIssue.lean
  737. forParallel.lean
  738. french_quote.lean
  739. frontend_meeting_2022_09_13.lean
  740. fun.lean
  741. funext.lean
  742. funind_demo.lean
  743. funind_expr.lean
  744. funind_fewer_levels.lean
  745. funind_mutual_dep.lean
  746. funind_proof.lean
  747. funind_structural.lean
  748. funind_structural_mutual.lean
  749. funind_tests.lean
  750. funMatchIssue.lean
  751. generalize.lean
  752. generalizeMany.lean
  753. generalizeTelescope.lean
  754. genindices.lean
  755. getline_crash.lean
  756. grind_cases.lean
  757. grind_pre.lean
  758. grind_revertAll.lean
  759. guard_expr.lean
  760. guard_msgs.lean
  761. guardexpr.lean
  762. handleLocking.lean
  763. hashableBug.lean
  764. hashmap-implicits.lean
  765. hashmap.lean
  766. haveDestruct.lean
  767. haveI.lean
  768. haveTactic.lean
  769. hcongr.lean
  770. heapSort.lean
  771. heqSubst.lean
  772. hlistOverload.lean
  773. hmul2.lean
  774. hmulDefaultIntance.lean
  775. ifcongr.lean
  776. iffRefl.lean
  777. ifThenElseIssue.lean
  778. ifThenElseIssue2.lean
  779. impByNameResolution.lean
  780. impLambdaTac.lean
  781. implicitApplyIssue.lean
  782. implicitLambdaLocalWithoutType.lean
  783. implicitTypesRecCoe.lean
  784. inaccessibleAnnotDefEqIssue.lean
  785. incmd.lean
  786. ind_cmd_bug.lean
  787. ind_whnf.lean
  788. ind_whnf2.lean
  789. induction1.lean
  790. inductionAltExplicit.lean
  791. inductionCheckAltNames.lean
  792. inductionLetIssue.lean
  793. inductionParse.lean
  794. inductionTacticBug.lean
  795. inductive1.lean
  796. inductive2.lean
  797. inductive_pred.lean
  798. inductive_rec_proj.lean
  799. inductive_typestar.lean
  800. inductiveIndicesIssue.lean
  801. indUsingLet.lean
  802. inferForallTypeLCNF.lean
  803. infixprio.lean
  804. inj1.lean
  805. inj2.lean
  806. injectionBug.lean
  807. injections1.lean
  808. injectionsIssue.lean
  809. injective.lean
  810. injHEq.lean
  811. injIssue.lean
  812. injSimp.lean
  813. inline_fn.lean
  814. inlineIfReduceLCNF.lean
  815. inlineLCNFIssue.lean
  816. inlineLoop.lean
  817. inlineProjInstIssue.lean
  818. inliner_loop.lean
  819. inlineWithNestedRecIssue.lean
  820. instanceIssues.lean
  821. instances.lean
  822. instanceWhere.lean
  823. instanceWhereDecls.lean
  824. instEtaIssue.lean
  825. instPatVar.lean
  826. instprio.lean
  827. instuniv.lean
  828. int_complement_shiftRight.lean
  829. int_to_nat_bug.lean
  830. internalizeCasesIssue.lean
  831. interp.lean
  832. interp2.lean
  833. introLetFun.lean
  834. intromacro.lean
  835. IO_test.lean
  836. ioRandomBytes.lean
  837. irCompilerBug.lean
  838. irreducibleIssue.lean
  839. isDefEqCheckAssignmentBug.lean
  840. isDefEqConstApproxIssue.lean
  841. isDefEqIssue.lean
  842. isDefEqMVarSelfIssue.lean
  843. isDefEqPerfIssue.lean
  844. isDefEqProjIssue.lean
  845. isDefEqProjPerfIssue.lean
  846. issue2628.lean
  847. issue2883.lean
  848. issue2925.lean
  849. issue2975.lean
  850. issue2982.lean
  851. issue3175.lean
  852. issue3204.lean
  853. issue3212.lean
  854. issue3770.lean
  855. issue3848.lean
  856. issue4063.lean
  857. issue4146.lean
  858. issue4394.lean
  859. issue4540.lean
  860. issue4650.lean
  861. issue4671.lean
  862. issue4684.lean
  863. issue4726.lean
  864. issue5027.lean
  865. issue5061.lean
  866. issue5347.lean
  867. issue5384.lean
  868. issue5562.lean
  869. issue5602.lean
  870. issue5630.lean
  871. issue5661.lean
  872. issue5699.lean
  873. issue5726.lean
  874. issue5767.lean
  875. issue5828.lean
  876. issue5836.lean
  877. issue5903.lean
  878. ite_dsimproc.lean
  879. james1.lean
  880. jason1.lean
  881. json.lean
  882. json_empty.lean
  883. kernel1.lean
  884. kernel2.lean
  885. kernel_maxheartbeats.lean
  886. kernelInterrupt.lean
  887. kevin.lean
  888. krivine.lean
  889. kronRWIssue.lean
  890. KyleAlg.lean
  891. KyleAlgAbbrev.lean
  892. lazyListRotateUnfoldProof.lean
  893. lazylistThunk.lean
  894. lazyUnfoldingPerfIssue.lean
  895. lcnf1.lean
  896. lcnf2.lean
  897. lcnf3.lean
  898. lcnf4.lean
  899. lcnf_simp_let.lean
  900. lcnfBinderNameBug.lean
  901. lcnfCastIssue.lean
  902. lcnfCheckIssue.lean
  903. lcnfEtaExpandBug.lean
  904. lcnfInferProjTypeBug.lean
  905. lcnfInferProjTypeIssue.lean
  906. lcnfInliningIssue.lean
  907. lcnfIssue.lean
  908. lean3_zulip_issues_1.lean
  909. lean_nat_bitwise.lean
  910. lean_nat_gcd.lean
  911. left_right.lean
  912. lemma.lean
  913. let_Issue.lean
  914. letBRecOnIssue.lean
  915. letDeclSimp.lean
  916. letMVar.lean
  917. letrecInProofs.lean
  918. letrecInThm.lean
  919. letrecWFIssue.lean
  920. level.lean
  921. levelNamesInTacticMode.lean
  922. levelNGen.lean
  923. lex.lean
  924. libuv.lean
  925. liftMethodInMacrosIssue.lean
  926. LiftMethodIssue.lean
  927. linearByRefl.lean
  928. linearCategory_perf_issue.lean
  929. list_simp.lean
  930. listDecEq.lean
  931. listtostring.lean
  932. litToCtor.lean
  933. localNameResolutionWithProj.lean
  934. localParsers.lean
  935. lrat_roundtrip.lean
  936. macro.lean
  937. macro2.lean
  938. macro3.lean
  939. macro_macro.lean
  940. macroid.lean
  941. macroParams.lean
  942. manyAritySyntax.lean
  943. mapTR.lean
  944. match1.lean
  945. match_expr.lean
  946. match_expr_expected_type_issue.lean
  947. match_expr_meta_modifier.lean
  948. match_expr_perf.lean
  949. match_int_lit_issue.lean
  950. match_lit_fin_cover.lean
  951. match_lit_issues.lean
  952. match_lit_regression.lean
  953. match_unit.lean
  954. matchArrayLit.lean
  955. matchDiscrType.lean
  956. matchEqnsHEqIssue.lean
  957. matchEqs.lean
  958. matchEqsBug.lean
  959. matcherElimUniv.lean
  960. matchGenBug.lean
  961. matchGenIssue.lean
  962. matchNoPostponing.lean
  963. matchRw.lean
  964. matchtac.lean
  965. matchUnifyBug.lean
  966. matchVarIssue.lean
  967. matchWithSearch.lean
  968. mathlibetaissue.lean
  969. mathport18.lean
  970. mathport_issue16.lean
  971. matrix.lean
  972. may_postpone_tc.lean
  973. maze.lean
  974. mergeSort.lean
  975. mergeSortCPDT.lean
  976. messageKind.lean
  977. meta.lean
  978. meta1.lean
  979. meta2.lean
  980. meta3.lean
  981. meta4.lean
  982. meta5.lean
  983. meta6.lean
  984. meta7.lean
  985. methodsRetInhabited.lean
  986. Miller1.lean
  987. missingDeclName.lean
  988. missingExplicitWithForwardNamedDep.lean
  989. missingSizeOfArrayGetThm.lean
  990. mixedMacroRules.lean
  991. mixfix.lean
  992. mjissue.lean
  993. modAsClasses.lean
  994. monadCache.lean
  995. monadControl.lean
  996. MonadControl_tutorial.lean
  997. monotone.lean
  998. mulcomm.lean
  999. multiTargetCasesInductionIssue.lean
  1000. mut_ind_wf.lean
  1001. mutualDefThms.lean
  1002. mutualWithCompositeNames.lean
  1003. mutwf1.lean
  1004. mutwf2.lean
  1005. mutwf3.lean
  1006. mutwf4.lean
  1007. namePatEqThm.lean
  1008. namespaceHyg.lean
  1009. namespaceIssue.lean
  1010. namespaceResolution.lean
  1011. nary_nomatch.lean
  1012. nat_mod_defeq.lean
  1013. nativeReflBackdoor.lean
  1014. natlit.lean
  1015. nested_inductive.lean
  1016. nested_match_bug.lean
  1017. nestedDo.lean
  1018. nestedInductiveConstructions.lean
  1019. nestedInductiveIssue.lean
  1020. nestedInductiveRecType.lean
  1021. nestedIssueMatch.lean
  1022. nestedrec.lean
  1023. nestedtc.lean
  1024. nestedTypeFormers.lean
  1025. nestedWF.lean
  1026. new_compiler.lean
  1027. new_frontend2.lean
  1028. new_inductive.lean
  1029. new_inductive2.lean
  1030. newfrontend1.lean
  1031. newfrontend2.lean
  1032. newfrontend3.lean
  1033. newfrontend5.lean
  1034. nicerNestedDos.lean
  1035. no_simproc_usize.lean
  1036. nofun1.lean
  1037. noindexAnnotation.lean
  1038. nomatch_regression.lean
  1039. nomatch_tac.lean
  1040. noncomp.lean
  1041. noncomputable_bug.lean
  1042. nonrec.lean
  1043. norm_cast.lean
  1044. numChars.lean
  1045. obtain.lean
  1046. offsetIssue.lean
  1047. ofNat_class.lean
  1048. ofNatNormNum.lean
  1049. omega.lean
  1050. omega_examples.lean
  1051. omegaCanon.lean
  1052. omegaDischarger.lean
  1053. openInScopeBug.lean
  1054. openTermTactic.lean
  1055. optParam.lean
  1056. Ord.lean
  1057. overAndPartialAppsAtWF.lean
  1058. overloaded.lean
  1059. overloadsAndDelayedCoercions.lean
  1060. panicAtCheckAssignment.lean
  1061. parray1.lean
  1062. parsePrelude.lean
  1063. parserAliasShadow.lean
  1064. parserQuot.lean
  1065. partial1.lean
  1066. partialApp.lean
  1067. partialDelta.lean
  1068. patbug.lean
  1069. pendingInstBug.lean
  1070. pendingMVarIssue.lean
  1071. postponeBinRelIssue.lean
  1072. posView.lean
  1073. ppMaxSteps.lean
  1074. ppMVars.lean
  1075. PProd_syntax.lean
  1076. PPTopDownAnalyze.lean
  1077. ppUsingAnonymousConstructor.lean
  1078. precDSL.lean
  1079. primProjEtaIssue.lean
  1080. print_cmd.lean
  1081. printDecls.lean
  1082. printEqns.lean
  1083. prioDSL.lean
  1084. privateCtor.lean
  1085. processGenDiseqBug.lean
  1086. proj_delta_issue.lean
  1087. projDefEq2.lean
  1088. proofDataConfusionBug.lean
  1089. proofIrrelFVar.lean
  1090. propagateExpectedType.lean
  1091. prv.lean
  1092. psumAtWF.lean
  1093. ptrAddr.lean
  1094. qualifiedNamesRec.lean
  1095. quasi_pattern_unification_approx_issue.lean
  1096. quotInd.lean
  1097. range.lean
  1098. rational.lean
  1099. rawStrings.lean
  1100. rc_tests.lean
  1101. rcases.lean
  1102. rcases1.lean
  1103. readerThe.lean
  1104. recCommonPrefixAlpha.lean
  1105. recInfo1.lean
  1106. reduce1.lean
  1107. reduce2.lean
  1108. reduce3.lean
  1109. reducibilityAttrValidation.lean
  1110. reductionBug.lean
  1111. refl.lean
  1112. reflectiveIndPred.lean
  1113. regressions3210.lean
  1114. Reid1.lean
  1115. renameI.lean
  1116. renaming.lean
  1117. Reparen.lean
  1118. repeat.lean
  1119. repeatConv.lean
  1120. replace.lean
  1121. replace_tac.lean
  1122. repr_empty.lean
  1123. reserved.lean
  1124. reservedNameResolution.lean
  1125. resolveLVal.lean
  1126. returnOptIssue.lean
  1127. revert1.lean
  1128. rewrite.lean
  1129. rewrites.lean
  1130. rflApplyFoApprox.lean
  1131. rflProofsCongrCastsIssue.lean
  1132. rflReducibility.lean
  1133. rflTacticErrors.lean
  1134. robinson.lean
  1135. root.lean
  1136. rossel1.lean
  1137. run_cmd.lean
  1138. run_meta1.lean
  1139. rw_inst_implicit_args.lean
  1140. rw_inst_mvars.lean
  1141. rwRegression.lean
  1142. safeExp.lean
  1143. sarray.lean
  1144. scc.lean
  1145. scopedCommandAfterOpen.lean
  1146. scopedHindingIssue.lean
  1147. scopedLocalReducibility.lean
  1148. scopedParsers.lean
  1149. scopedParsers2.lean
  1150. scopedunifhint.lean
  1151. sealCommand.lean
  1152. secVarBug.lean
  1153. set.lean
  1154. set_lit_unexpand.lean
  1155. setOptionTermTactic.lean
  1156. setStructInstNotation.lean
  1157. seval1.lean
  1158. sharecommon.lean
  1159. show_term.lean
  1160. showTests.lean
  1161. shrinkFn.lean
  1162. sigmaprec.lean
  1163. sign.lean
  1164. simp-elab-recover.lean
  1165. simp1.lean
  1166. simp2.lean
  1167. simp3.lean
  1168. simp4.lean
  1169. simp5.lean
  1170. simp6.lean
  1171. simp_all.lean
  1172. simp_all_contextual.lean
  1173. simp_cache_perf_issue.lean
  1174. simp_eqn_bug.lean
  1175. simp_failIfUnchanged.lean
  1176. simp_inst_implict_args.lean
  1177. simp_proj_transparency_issue.lean
  1178. simpArith1.lean
  1179. simpArithCacheIssue.lean
  1180. simpAtDefIssue.lean
  1181. simpAutoUnfold.lean
  1182. simpBool.lean
  1183. simpBug.lean
  1184. simpCasesOnCtorBug.lean
  1185. simpCnstr1.lean
  1186. simpCondLemma.lean
  1187. simpDecide.lean
  1188. simpDefToUnfold.lean
  1189. simpDiag.lean
  1190. simpDischargeLoop.lean
  1191. simpExpBlowup.lean
  1192. simpExtraArgsBug.lean
  1193. simpGround1.lean
  1194. simpHigherOrder.lean
  1195. simpIfPre.lean
  1196. simpImpLocal.lean
  1197. simpIndexDiag.lean
  1198. simpInv.lean
  1199. simpIssue.lean
  1200. simpJpCasesDepBug.lean
  1201. simpLoopBug.lean
  1202. simpMatch.lean
  1203. simpMatchDiscr.lean
  1204. simpMatchDiscrIssue.lean
  1205. simpOnly.lean
  1206. simpPartialApp.lean
  1207. simpPreIssue.lean
  1208. simpPreprocess.lean
  1209. simpPrio.lean
  1210. simproc1.lean
  1211. simproc2.lean
  1212. simproc_builtin_erase.lean
  1213. simproc_disable_issue.lean
  1214. simproc_erase.lean
  1215. simproc_panic.lean
  1216. simproc_timeout.lean
  1217. simprocNat.lean
  1218. simpRwBug.lean
  1219. simpStar.lean
  1220. simpStarHyp.lean
  1221. simpUnfoldAbbrev.lean
  1222. sizeof1.lean
  1223. sizeof2.lean
  1224. sizeof3.lean
  1225. sizeof4.lean
  1226. sizeof5.lean
  1227. sizeof6.lean
  1228. skipAssignedInstances.lean
  1229. skipKernelTC.lean
  1230. smartUnfoldingBug.lean
  1231. solve_by_elim.lean
  1232. som1.lean
  1233. sorry.lean
  1234. spec_issue.lean
  1235. specbug.lean
  1236. specialize1.lean
  1237. specialize2.lean
  1238. specialize3.lean
  1239. split1.lean
  1240. split2.lean
  1241. split3.lean
  1242. splitAtCode.lean
  1243. splitIssue.lean
  1244. splitList.lean
  1245. starsAndBars.lean
  1246. state12.lean
  1247. state8.lean
  1248. stateRef.lean
  1249. streamEqIssue.lean
  1250. string.lean
  1251. string_gaps.lean
  1252. string_simprocs.lean
  1253. strInterpolation.lean
  1254. strLitProj.lean
  1255. struct1.lean
  1256. struct2.lean
  1257. struct3.lean
  1258. struct_inst_typed.lean
  1259. struct_instance_in_eqn.lean
  1260. structEqns.lean
  1261. structInst.lean
  1262. structInst2.lean
  1263. structInst3.lean
  1264. structInst4.lean
  1265. structInstFast.lean
  1266. structNoBody.lean
  1267. structPrivateFieldBug.lean
  1268. structPrivateFieldBug2.lean
  1269. structuralEqns.lean
  1270. structuralEqns2.lean
  1271. structuralEqns3.lean
  1272. structuralIssue.lean
  1273. structuralIssue2.lean
  1274. structuralMutual.lean
  1275. structuralOverNested.lean
  1276. structuralRec1.lean
  1277. structure.lean
  1278. structure_recursive.lean
  1279. structWithAlgTCSynth.lean
  1280. stuckMVarBug.lean
  1281. stuckTC.lean
  1282. stxKindInsideNamespace.lean
  1283. stxMacro.lean
  1284. subarray_split.lean
  1285. subarray_split.lean.expected.out
  1286. subexpr.lean
  1287. subset.lean
  1288. subst.lean
  1289. subst1.lean
  1290. substVars.lean
  1291. substWithoutExpectedType.lean
  1292. subtype_inj.lean
  1293. suffices.lean
  1294. symm.lean
  1295. syntax1.lean
  1296. syntaxAbbrevQuot.lean
  1297. syntaxPrio.lean
  1298. synth1.lean
  1299. synthInstsIssue.lean
  1300. synthOrderRegression.lean
  1301. synthPending1.lean
  1302. synthPendingBug.lean
  1303. tactic.lean
  1304. tactic1.lean
  1305. tactic_config.lean
  1306. tacticDoc.lean
  1307. tacticExtOverlap.lean
  1308. tacticTests.lean
  1309. takeSimpEqns.lean
  1310. task_test.lean
  1311. task_test2.lean
  1312. task_test_io.lean
  1313. taskState.lean
  1314. tc_eta_struct_issue.lean
  1315. tcUnivIssue.lean
  1316. tempfile.lean
  1317. termElab.lean
  1318. terminationByStructurally.lean
  1319. termParserAttr.lean
  1320. TermSeq.lean
  1321. test_single.sh
  1322. thmIsProp.lean
  1323. time.lean
  1324. toArrayEq.lean
  1325. toDeclEtaBug.lean
  1326. toExpr.lean
  1327. toFromJson.lean
  1328. toLCNFCacheBug.lean
  1329. trace.lean
  1330. traceElabIssue.lean
  1331. trans.lean
  1332. treeNode.lean
  1333. trivial_uint.lean
  1334. tryHeuristicPerfIssue.lean
  1335. tryHeuristicPerfIssue2.lean
  1336. tryPostponeIssue.lean
  1337. type_class_performance1.lean
  1338. typeAscImp.lean
  1339. typeclass_append.lean
  1340. typeclass_coerce.lean
  1341. typeclass_diamond.lean
  1342. typeclass_easy.lean
  1343. typeclass_loop.lean
  1344. typeclass_metas_internal_goals1.lean
  1345. typeclass_metas_internal_goals2.lean
  1346. typeclass_metas_internal_goals3.lean
  1347. typeclass_metas_internal_goals4.lean
  1348. typeclass_outparam.lean
  1349. typeOccursCheckIssue.lean
  1350. ubscalar.lean
  1351. unexpected_result_with_bind.lean
  1352. unfoldLemma.lean
  1353. unfoldMany.lean
  1354. unfoldPartialRegression.lean
  1355. unfoldr.lean
  1356. unfoldTactic.lean
  1357. unif_issue.lean
  1358. unif_issue2.lean
  1359. unifhint1.lean
  1360. unifhint2.lean
  1361. unifhint3.lean
  1362. unihint.lean
  1363. univCnstrApprox.lean
  1364. univIssue.lean
  1365. univParamIssue.lean
  1366. univPolyEnum.lean
  1367. unsafeConst.lean
  1368. unsafeInit.lean
  1369. unsafeTerm.lean
  1370. update.lean
  1371. utf8英語.lean
  1372. variable.lean
  1373. wfEqns1.lean
  1374. wfEqns2.lean
  1375. wfEqns3.lean
  1376. wfEqns4.lean
  1377. wfEqns5.lean
  1378. wfEqnsIssue.lean
  1379. wfForIn.lean
  1380. wfirred.lean
  1381. wfLean3Issue.lean
  1382. wfOmega.lean
  1383. wfOverapplicationIssue.lean
  1384. wfrecUnary.lean
  1385. WFRelSearch.lean
  1386. wfSum.lean
  1387. where1.lean
  1388. whereCmd.lean
  1389. whileRepeat.lean
  1390. whnfDelayedMVarIssue.lean
  1391. WindowsNewlines.lean
  1392. withReducibleAndInstancesCrash.lean
  1393. zeroExitPoints.lean
  1394. zetaDelta.lean
  1395. zetaDeltaIssue.lean
  1396. zetaDSimpIssue.lean