tree: 0e660e6c9db2f13860ab448efdad0a463dab54c4 [search]
  1. interactive/
  2. Reformat/
  3. run/
  4. server/
  5. trust0/
  6. .gitignore
  7. 1007.lean
  8. 1007.lean.expected.out
  9. 1011.lean
  10. 1011.lean.expected.out
  11. 1018unknowMVarIssue.lean
  12. 1018unknowMVarIssue.lean.expected.out
  13. 1021.lean
  14. 1021.lean.expected.out
  15. 1026.lean
  16. 1026.lean.expected.out
  17. 1027.lean
  18. 1027.lean.expected.out
  19. 1038.lean
  20. 1038.lean.expected.out
  21. 1039.lean
  22. 1039.lean.expected.out
  23. 1050.lean
  24. 1050.lean.expected.out
  25. 1057.lean
  26. 1057.lean.expected.out
  27. 1062.lean
  28. 1062.lean.expected.out
  29. 1074a.lean
  30. 1074a.lean.expected.out
  31. 1074b.lean
  32. 1074b.lean.expected.out
  33. 1079.lean
  34. 1079.lean.expected.out
  35. 1081.lean
  36. 1081.lean.expected.out
  37. 1098.lean
  38. 1098.lean.expected.out
  39. 1102.lean
  40. 1102.lean.expected.out
  41. 1112.lean
  42. 1112.lean.expected.out
  43. 1113.lean
  44. 1113.lean.expected.out
  45. 1163.lean
  46. 1163.lean.expected.out
  47. 1206.lean
  48. 1206.lean.expected.out
  49. 1235.lean
  50. 1235.lean.expected.out
  51. 1240.lean
  52. 1240.lean.expected.out
  53. 1275.lean
  54. 1275.lean.expected.out
  55. 1279.lean
  56. 1279.lean.expected.out
  57. 1279_simplified.lean
  58. 1279_simplified.lean.expected.out
  59. 1292.lean
  60. 1292.lean.expected.out
  61. 1298.lean
  62. 1298.lean.expected.out
  63. 1301.lean
  64. 1301.lean.expected.out
  65. 1321.lean
  66. 1321.lean.expected.out
  67. 1358.lean
  68. 1358.lean.expected.out
  69. 1363.lean
  70. 1363.lean.expected.out
  71. 1367.lean
  72. 1367.lean.expected.out
  73. 1371.lean
  74. 1371.lean.expected.out
  75. 1377.lean
  76. 1377.lean.expected.out
  77. 1433.lean
  78. 1433.lean.expected.out
  79. 1569.lean
  80. 1569.lean.expected.out
  81. 1571.lean
  82. 1571.lean.expected.out
  83. 1576.lean
  84. 1576.lean.expected.out
  85. 1606.lean
  86. 1606.lean.expected.out
  87. 1657.lean
  88. 1657.lean.expected.out
  89. 1668.lean
  90. 1668.lean.expected.out
  91. 1673.lean
  92. 1673.lean.expected.out
  93. 1681.lean
  94. 1681.lean.expected.out
  95. 1682.lean
  96. 1682.lean.expected.out
  97. 1690.lean
  98. 1690.lean.expected.out
  99. 1705.lean
  100. 1705.lean.expected.out
  101. 1707.lean
  102. 1707.lean.expected.out
  103. 1719.lean
  104. 1719.lean.expected.out
  105. 1760.lean
  106. 1760.lean.expected.out
  107. 1763.lean
  108. 1763.lean.expected.out
  109. 1779.lean
  110. 1779.lean.expected.out
  111. 1781.lean
  112. 1781.lean.expected.out
  113. 1804.lean
  114. 1804.lean.expected.out
  115. 1825.lean
  116. 1825.lean.expected.out
  117. 1845.lean
  118. 1845.lean.expected.out
  119. 1856.lean
  120. 1856.lean.expected.out
  121. 1870.lean
  122. 1870.lean.expected.out
  123. 1878.lean
  124. 1878.lean.expected.out
  125. 1891.lean
  126. 1891.lean.expected.out
  127. 2005.lean
  128. 2005.lean.expected.out
  129. 2006.lean
  130. 2006.lean.expected.out
  131. 2040.lean
  132. 2040.lean.expected.out
  133. 2045.lean
  134. 2045.lean.expected.out
  135. 2125.lean
  136. 2125.lean.expected.out
  137. 217.lean
  138. 217.lean.expected.out
  139. 220.lean
  140. 220.lean.expected.out
  141. 223.lean
  142. 223.lean.expected.out
  143. 236.lean
  144. 236.lean.expected.out
  145. 241.lean
  146. 241.lean.expected.out
  147. 242.lean
  148. 242.lean.expected.out
  149. 243.lean
  150. 243.lean.expected.out
  151. 247.lean
  152. 247.lean.expected.out
  153. 248.lean
  154. 248.lean.expected.out
  155. 255.lean
  156. 255.lean.expected.out
  157. 276.lean
  158. 276.lean.expected.out
  159. 277a.lean
  160. 277a.lean.expected.out
  161. 277b.lean
  162. 277b.lean.expected.out
  163. 283.lean
  164. 283.lean.expected.out
  165. 297.lean
  166. 297.lean.expected.out
  167. 301.lean
  168. 301.lean.expected.out
  169. 302.lean
  170. 302.lean.expected.out
  171. 307.lean
  172. 307.lean.expected.out
  173. 309.lean
  174. 309.lean.expected.out
  175. 331.lean
  176. 331.lean.expected.out
  177. 343.lean
  178. 343.lean.expected.out
  179. 345.lean
  180. 345.lean.expected.out
  181. 346.lean
  182. 346.lean.expected.out
  183. 348.lean
  184. 348.lean.expected.out
  185. 353.lean
  186. 353.lean.expected.out
  187. 361.lean
  188. 361.lean.expected.out
  189. 366.lean
  190. 366.lean.expected.out
  191. 386.lean
  192. 386.lean.expected.out
  193. 389.lean
  194. 389.lean.expected.out
  195. 414.lean
  196. 414.lean.expected.out
  197. 415.lean
  198. 415.lean.expected.out
  199. 421.lean
  200. 421.lean.expected.out
  201. 423.lean
  202. 423.lean.expected.out
  203. 435.lean
  204. 435.lean.expected.out
  205. 435b.lean
  206. 435b.lean.expected.out
  207. 439.lean
  208. 439.lean.expected.out
  209. 440.lean
  210. 440.lean.expected.out
  211. 445.lean
  212. 445.lean.expected.out
  213. 448.lean
  214. 448.lean.expected.out
  215. 449.lean
  216. 449.lean.expected.out
  217. 450.lean
  218. 450.lean.expected.out
  219. 456.lean
  220. 456.lean.expected.out
  221. 469.lean
  222. 469.lean.expected.out
  223. 474.lean
  224. 474.lean.expected.out
  225. 490.lean
  226. 490.lean.expected.out
  227. 496.lean
  228. 496.lean.expected.out
  229. 529.lean
  230. 529.lean.expected.out
  231. 550.lean
  232. 550.lean.expected.out
  233. 586.lean
  234. 586.lean.expected.out
  235. 593.lean
  236. 593.lean.expected.out
  237. 603.lean
  238. 603.lean.expected.out
  239. 604.lean
  240. 604.lean.expected.out
  241. 620.lean
  242. 620.lean.expected.out
  243. 621.lean
  244. 621.lean.expected.out
  245. 625.lean
  246. 625.lean.expected.out
  247. 641.lean
  248. 641.lean.expected.out
  249. 653.lean
  250. 653.lean.expected.out
  251. 655.lean
  252. 655.lean.expected.out
  253. 679.lean
  254. 679.lean.expected.out
  255. 689.lean
  256. 689.lean.expected.out
  257. 690.lean
  258. 690.lean.expected.out
  259. 697.lean
  260. 697.lean.expected.out
  261. 714.lean
  262. 714.lean.expected.out
  263. 755.lean
  264. 755.lean.expected.out
  265. 770.lean
  266. 770.lean.expected.out
  267. 799.lean
  268. 799.lean.expected.out
  269. 801.lean
  270. 801.lean.expected.out
  271. 813.lean
  272. 813.lean.expected.out
  273. 815b.lean
  274. 815b.lean.expected.out
  275. 906.lean
  276. 906.lean.expected.out
  277. 916.lean
  278. 916.lean.expected.out
  279. 948.lean
  280. 948.lean.expected.out
  281. 951.lean
  282. 951.lean.expected.out
  283. 973.lean
  284. 973.lean.expected.out
  285. 973b.lean
  286. 973b.lean.expected.out
  287. 974.lean
  288. 974.lean.expected.out
  289. 986.lean
  290. 986.lean.expected.out
  291. 995.lean
  292. 995.lean.expected.out
  293. abst.lean
  294. abst.lean.expected.out
  295. allFieldForConstants.lean
  296. allFieldForConstants.lean.expected.out
  297. ambiguousOpenExport.lean
  298. ambiguousOpenExport.lean.expected.out
  299. antiquotRecovery.lean
  300. antiquotRecovery.lean.expected.out
  301. appParserIssue.lean
  302. appParserIssue.lean.expected.out
  303. argNameAtPlaceholderError.lean
  304. argNameAtPlaceholderError.lean.expected.out
  305. argNameIfMacroScopes.lean
  306. argNameIfMacroScopes.lean.expected.out
  307. arrayGetU.lean
  308. arrayGetU.lean.expected.out
  309. attrCmd.lean
  310. attrCmd.lean.expected.out
  311. autobound_and_macroscopes.lean
  312. autobound_and_macroscopes.lean.expected.out
  313. autoBoundErrorMsg.lean
  314. autoBoundErrorMsg.lean.expected.out
  315. autoBoundImplicits1.lean
  316. autoBoundImplicits1.lean.expected.out
  317. autoBoundImplicits2.lean
  318. autoBoundImplicits2.lean.expected.out
  319. autoBoundPostponeLoop.lean
  320. autoBoundPostponeLoop.lean.expected.out
  321. autoImplicitChain.lean
  322. autoImplicitChain.lean.expected.out
  323. autoImplicitChainNameIssue.lean
  324. autoImplicitChainNameIssue.lean.expected.out
  325. autoImplicitCtorParamIssue.lean
  326. autoImplicitCtorParamIssue.lean.expected.out
  327. autoImplicitForbidden.lean
  328. autoImplicitForbidden.lean.expected.out
  329. autoIssue.lean
  330. autoIssue.lean.expected.out
  331. autoPPExplicit.lean
  332. autoPPExplicit.lean.expected.out
  333. auxDeclIssue.lean
  334. auxDeclIssue.lean.expected.out
  335. badBinderName.lean
  336. badBinderName.lean.expected.out
  337. badIhName.lean
  338. badIhName.lean.expected.out
  339. baseIO.lean
  340. baseIO.lean.expected.out
  341. beginEndAsMacro.lean
  342. beginEndAsMacro.lean.expected.out
  343. bigUnivOffsets.lean
  344. bigUnivOffsets.lean.expected.out
  345. binderCacheIssue.lean
  346. binderCacheIssue.lean.expected.out
  347. binderCacheIssue2.lean
  348. binderCacheIssue2.lean.expected.out
  349. bindersAbstractingUnassignedMVars.lean
  350. bindersAbstractingUnassignedMVars.lean.expected.out
  351. binop_lazy.lean
  352. binop_lazy.lean.expected.out
  353. binopInfoTree.lean
  354. binopInfoTree.lean.expected.out
  355. binopIssues.lean
  356. binopIssues.lean.expected.out
  357. binrel_binop.lean
  358. binrel_binop.lean.expected.out
  359. binsearch.lean
  360. binsearch.lean.expected.out
  361. bintreeGoal.lean
  362. bintreeGoal.lean.expected.out
  363. bitwise.lean
  364. bitwise.lean.expected.out
  365. byCasesMetaM.lean
  366. byCasesMetaM.lean.expected.out
  367. byStrictIndent.lean
  368. byStrictIndent.lean.expected.out
  369. bytearray.lean
  370. bytearray.lean.expected.out
  371. cacheIssue.lean
  372. cacheIssue.lean.expected.out
  373. calcErrors.lean
  374. calcErrors.lean.expected.out
  375. casesOnCases.lean
  376. casesOnCases.lean.expected.out
  377. cdotAtSimpArg.lean
  378. cdotAtSimpArg.lean.expected.out
  379. cdotTuple.lean
  380. cdotTuple.lean.expected.out
  381. class_def_must_fail.lean
  382. class_def_must_fail.lean.expected.out
  383. classBadOutParam.lean
  384. classBadOutParam.lean.expected.out
  385. collectDepsIssue.lean
  386. collectDepsIssue.lean.expected.out
  387. commandPrefix.lean
  388. commandPrefix.lean.expected.out
  389. CompilerConstantFold.lean
  390. CompilerConstantFold.lean.expected.out
  391. CompilerElimDeadBranches.lean
  392. CompilerElimDeadBranches.lean.expected.out
  393. CompilerProvokeFloatLet.lean
  394. CompilerProvokeFloatLet.lean.expected.out
  395. computedFieldsCode.lean
  396. computedFieldsCode.lean.expected.out
  397. congrThm.lean
  398. congrThm.lean.expected.out
  399. congrThmIssue.lean
  400. congrThmIssue.lean.expected.out
  401. constDelab.lean
  402. constDelab.lean.expected.out
  403. constructorTac.lean
  404. constructorTac.lean.expected.out
  405. consumePPHint.lean
  406. consumePPHint.lean.expected.out
  407. conv1.lean
  408. conv1.lean.expected.out
  409. convInConv.lean
  410. convInConv.lean.expected.out
  411. convPatternAtLetIssue.lean
  412. convPatternAtLetIssue.lean.expected.out
  413. convPatternMatchIssue.lean
  414. convPatternMatchIssue.lean.expected.out
  415. convZetaLetExt.lean
  416. convZetaLetExt.lean.expected.out
  417. copy-produced
  418. csimpAttr.lean
  419. csimpAttr.lean.expected.out
  420. csimpAttrAppend.lean
  421. csimpAttrAppend.lean.expected.out
  422. ctor_layout.lean
  423. ctor_layout.lean.expected.out
  424. ctorUnivTooBig.lean
  425. ctorUnivTooBig.lean.expected.out
  426. dbgMacros.lean
  427. dbgMacros.lean.expected.out
  428. decimals.lean
  429. decimals.lean.expected.out
  430. decreasing_by.lean
  431. decreasing_by.lean.expected.out
  432. defaultInstance.lean
  433. defaultInstance.lean.expected.out
  434. defaultInstanceWithPrio.lean
  435. defaultInstanceWithPrio.lean.expected.out
  436. defInst.lean
  437. defInst.lean.expected.out
  438. delabUnexpand.lean
  439. delabUnexpand.lean.expected.out
  440. delta.lean
  441. delta.lean.expected.out
  442. deprecated.lean
  443. deprecated.lean.expected.out
  444. derivingDecidableEq.lean
  445. derivingDecidableEq.lean.expected.out
  446. derivingHashable.lean
  447. derivingHashable.lean.expected.out
  448. derivingRepr.lean
  449. derivingRepr.lean.expected.out
  450. derivingRpcEncoding.lean
  451. derivingRpcEncoding.lean.expected.out
  452. diamond1.lean
  453. diamond1.lean.expected.out
  454. diamond10.lean
  455. diamond10.lean.expected.out
  456. diamond2.lean
  457. diamond2.lean.expected.out
  458. diamond3.lean
  459. diamond3.lean.expected.out
  460. diamond4.lean
  461. diamond4.lean.expected.out
  462. diamond5.lean
  463. diamond5.lean.expected.out
  464. diamond6.lean
  465. diamond6.lean.expected.out
  466. diamond7.lean
  467. diamond7.lean.expected.out
  468. diamond8.lean
  469. diamond8.lean.expected.out
  470. diamond9.lean
  471. diamond9.lean.expected.out
  472. discrTreeIota.lean
  473. discrTreeIota.lean.expected.out
  474. docStr.lean
  475. docStr.lean.expected.out
  476. doErrorMsg.lean
  477. doErrorMsg.lean.expected.out
  478. doIfLet.lean
  479. doIfLet.lean.expected.out
  480. doIssue.lean
  481. doIssue.lean.expected.out
  482. doLetLoop.lean
  483. doLetLoop.lean.expected.out
  484. doNotation1.lean
  485. doNotation1.lean.expected.out
  486. doSeqRightIssue.lean
  487. doSeqRightIssue.lean.expected.out
  488. dsimpZetaIssue.lean
  489. dsimpZetaIssue.lean.expected.out
  490. eagerCoeExpansion.lean
  491. eagerCoeExpansion.lean.expected.out
  492. eagerUnfoldingIssue.lean
  493. eagerUnfoldingIssue.lean.expected.out
  494. elabAsElim.lean
  495. elabAsElim.lean.expected.out
  496. ellipsisProjIssue.lean
  497. ellipsisProjIssue.lean.expected.out
  498. elseifDoErrorPos.lean
  499. elseifDoErrorPos.lean.expected.out
  500. emptyc.lean
  501. emptyc.lean.expected.out
  502. emptyTypeAscription.lean
  503. emptyTypeAscription.lean.expected.out
  504. eoi.lean
  505. eoi.lean.expected.out
  506. eqValue.lean
  507. eqValue.lean.expected.out
  508. eraseInsts.lean
  509. eraseInsts.lean.expected.out
  510. eraseSimp.lean
  511. eraseSimp.lean.expected.out
  512. errorOnInductionForNested.lean
  513. errorOnInductionForNested.lean.expected.out
  514. errorRecoveryBug.lean
  515. errorRecoveryBug.lean.expected.out
  516. eta.lean
  517. eta.lean.expected.out
  518. etaStructIssue.lean
  519. etaStructIssue.lean.expected.out
  520. eval_except.lean
  521. eval_except.lean.expected.out
  522. evalCmd.lean
  523. evalCmd.lean.expected.out
  524. evalInstMessage.lean
  525. evalInstMessage.lean.expected.out
  526. evalNone.lean
  527. evalNone.lean.expected.out
  528. evalSorry.lean
  529. evalSorry.lean.expected.out
  530. evalWithMVar.lean
  531. evalWithMVar.lean.expected.out
  532. exactErrorPos.lean
  533. exactErrorPos.lean.expected.out
  534. exitAfterParseError.lean
  535. exitAfterParseError.lean.expected.out
  536. expandExplicitBinders.lean
  537. expandExplicitBinders.lean.expected.out
  538. extract.lean
  539. extract.lean.expected.out
  540. failTac.lean
  541. failTac.lean.expected.out
  542. file_not_found.lean
  543. file_not_found.lean.expected.out
  544. filePath.lean
  545. filePath.lean.expected.out
  546. fixedIndexToParamIssue.lean
  547. fixedIndexToParamIssue.lean.expected.out
  548. fixedIndicesToParams.lean
  549. fixedIndicesToParams.lean.expected.out
  550. forallMetaBounded.lean
  551. forallMetaBounded.lean.expected.out
  552. forErrors.lean
  553. forErrors.lean.expected.out
  554. Format.lean
  555. Format.lean.expected.out
  556. formatTerm.lean
  557. formatTerm.lean.expected.out
  558. fun.lean
  559. fun.lean.expected.out
  560. funExpected.lean
  561. funExpected.lean.expected.out
  562. funInfoBug.lean
  563. funInfoBug.lean.expected.out
  564. funParen.lean
  565. funParen.lean.expected.out
  566. gcd.lean
  567. gcd.lean.expected.out
  568. getElem.lean
  569. getElem.lean.expected.out
  570. have.lean
  571. have.lean.expected.out
  572. heapSort.lean
  573. heapSort.lean.expected.out
  574. hidingInaccessibleNames.lean
  575. hidingInaccessibleNames.lean.expected.out
  576. holeErrors.lean
  577. holeErrors.lean.expected.out
  578. holes.lean
  579. holes.lean.expected.out
  580. hygienicIntro.lean
  581. hygienicIntro.lean.expected.out
  582. implementedByIssue.lean
  583. implementedByIssue.lean.expected.out
  584. implicitLambdaIssue.lean
  585. implicitLambdaIssue.lean.expected.out
  586. implicitTypePos.lean
  587. implicitTypePos.lean.expected.out
  588. inductionErrors.lean
  589. inductionErrors.lean.expected.out
  590. inductionGen.lean
  591. inductionGen.lean.expected.out
  592. inductionMutual.lean
  593. inductionMutual.lean.expected.out
  594. inductive1.lean
  595. inductive1.lean.expected.out
  596. inductiveUnivErrorMsg.lean
  597. inductiveUnivErrorMsg.lean.expected.out
  598. infoFromFailure.lean
  599. infoFromFailure.lean.expected.out
  600. inlineIssue.lean
  601. inlineIssue.lean.expected.out
  602. inst.lean
  603. inst.lean.expected.out
  604. instance1.lean
  605. instance1.lean.expected.out
  606. intModBug.lean
  607. intModBug.lean.expected.out
  608. intNegSucc.lean
  609. intNegSucc.lean.expected.out
  610. introLetBug.lean
  611. introLetBug.lean.expected.out
  612. invalidFieldName.lean
  613. invalidFieldName.lean.expected.out
  614. invalidInstImplicit.lean
  615. invalidInstImplicit.lean.expected.out
  616. invalidNamedArgs.lean
  617. invalidNamedArgs.lean.expected.out
  618. invalidPatternIssue.lean
  619. invalidPatternIssue.lean.expected.out
  620. IRbug.lean
  621. IRbug.lean.expected.out
  622. isDefEqOffsetBug.lean
  623. isDefEqOffsetBug.lean.expected.out
  624. isNoncomputable.lean
  625. isNoncomputable.lean.expected.out
  626. jason1.lean
  627. jason1.lean.expected.out
  628. jason2.lean
  629. jason2.lean.expected.out
  630. jpCasesDiscrM.lean
  631. jpCasesDiscrM.lean.expected.out
  632. jpCasesNary.lean
  633. jpCasesNary.lean.expected.out
  634. jpClosureIssue.lean
  635. jpClosureIssue.lean.expected.out
  636. json.lean
  637. json.lean.expected.out
  638. kernelMVarBug.lean
  639. kernelMVarBug.lean.expected.out
  640. keyAttrErase.lean
  641. keyAttrErase.lean.expected.out
  642. lambdaLiftCache.lean
  643. lambdaLiftCache.lean.expected.out
  644. lazySeq.lean
  645. lazySeq.lean.expected.out
  646. lcnfTypes.lean
  647. lcnfTypes.lean.expected.out
  648. LE.lean
  649. LE.lean.expected.out
  650. lean3RefineBug.lean
  651. lean3RefineBug.lean.expected.out
  652. letArrowOutsideDo.lean
  653. letArrowOutsideDo.lean.expected.out
  654. letFun.lean
  655. letFun.lean.expected.out
  656. letPatIssue.lean
  657. letPatIssue.lean.expected.out
  658. letrec1.lean
  659. letrec1.lean.expected.out
  660. letrecErrors.lean
  661. letrecErrors.lean.expected.out
  662. letRecMissingAnnotation.lean
  663. letRecMissingAnnotation.lean.expected.out
  664. letRecTheorem.lean
  665. letRecTheorem.lean.expected.out
  666. levelNGen.lean
  667. levelNGen.lean.expected.out
  668. liftOverLeft.lean
  669. liftOverLeft.lean.expected.out
  670. linterMissingDocs.lean
  671. linterMissingDocs.lean.expected.out
  672. linterSuspiciousUnexpanderPatterns.lean
  673. linterSuspiciousUnexpanderPatterns.lean.expected.out
  674. linterUnusedVariables.lean
  675. linterUnusedVariables.lean.expected.out
  676. listLength.lean
  677. listLength.lean.expected.out
  678. ll_infer_type_bug.lean
  679. ll_infer_type_bug.lean.expected.out
  680. localNotationPP.lean
  681. localNotationPP.lean.expected.out
  682. longestParsePrio.lean
  683. longestParsePrio.lean.expected.out
  684. loopErrorRecovery.lean
  685. loopErrorRecovery.lean.expected.out
  686. lvl1.lean
  687. lvl1.lean.expected.out
  688. macroElabRulesIssue1.lean
  689. macroElabRulesIssue1.lean.expected.out
  690. macroElabRulesIssue2.lean
  691. macroElabRulesIssue2.lean.expected.out
  692. macroError.lean
  693. macroError.lean.expected.out
  694. macroPrio.lean
  695. macroPrio.lean.expected.out
  696. macroResolveName.lean
  697. macroResolveName.lean.expected.out
  698. macroscopes.lean
  699. macroscopes.lean.expected.out
  700. macroStack.lean
  701. macroStack.lean.expected.out
  702. macroSwizzle.lean
  703. macroSwizzle.lean.expected.out
  704. macroTrace.lean
  705. macroTrace.lean.expected.out
  706. magical.lean
  707. magical.lean.expected.out
  708. mangling.lean
  709. mangling.lean.expected.out
  710. match1.lean
  711. match1.lean.expected.out
  712. match2.lean
  713. match2.lean.expected.out
  714. match3.lean
  715. match3.lean.expected.out
  716. match4.lean
  717. match4.lean.expected.out
  718. matchAltIndent.lean
  719. matchAltIndent.lean.expected.out
  720. matchApp.lean
  721. matchApp.lean.expected.out
  722. matchErrorLocation.lean
  723. matchErrorLocation.lean.expected.out
  724. matchErrorMsg.lean
  725. matchErrorMsg.lean.expected.out
  726. matchLeftovers.lean
  727. matchLeftovers.lean.expected.out
  728. matchMissingCasesAsStuckError.lean
  729. matchMissingCasesAsStuckError.lean.expected.out
  730. matchMultAlt.lean
  731. matchMultAlt.lean.expected.out
  732. matchOfNatIssue.lean
  733. matchOfNatIssue.lean.expected.out
  734. matchOrIssue.lean
  735. matchOrIssue.lean.expected.out
  736. matchPatternInsideBinders.lean
  737. matchPatternInsideBinders.lean.expected.out
  738. matchPatternPartialApp.lean
  739. matchPatternPartialApp.lean.expected.out
  740. matchunit.lean
  741. matchunit.lean.expected.out
  742. matchUnknownFVarBug.lean
  743. matchUnknownFVarBug.lean.expected.out
  744. matchVarNames.lean
  745. matchVarNames.lean.expected.out
  746. metaEvalInstMessage.lean
  747. metaEvalInstMessage.lean.expected.out
  748. missingExplicitWithForwardNamedDep.lean
  749. missingExplicitWithForwardNamedDep.lean.expected.out
  750. mkProjStx.lean
  751. mkProjStx.lean.expected.out
  752. modBug.lean
  753. modBug.lean.expected.out
  754. moduleDoc.lean
  755. moduleDoc.lean.expected.out
  756. moduleOf.lean
  757. moduleOf.lean.expected.out
  758. mulcommErrorMessage.lean
  759. mulcommErrorMessage.lean.expected.out
  760. multiConstantError.lean
  761. multiConstantError.lean.expected.out
  762. mutualdef1.lean
  763. mutualdef1.lean.expected.out
  764. mutualWithNamespaceMacro.lean
  765. mutualWithNamespaceMacro.lean.expected.out
  766. mutwf1.lean
  767. mutwf1.lean.expected.out
  768. mvar_fvar.lean
  769. mvar_fvar.lean.expected.out
  770. mvarAtDefaultValue.lean
  771. mvarAtDefaultValue.lean.expected.out
  772. nameArgErrorIssue.lean
  773. nameArgErrorIssue.lean.expected.out
  774. namedHoles.lean
  775. namedHoles.lean.expected.out
  776. namelit.lean
  777. namelit.lean.expected.out
  778. namePatEqThm.lean
  779. namePatEqThm.lean.expected.out
  780. nameRepr.lean
  781. nameRepr.lean.expected.out
  782. negFloat.lean
  783. negFloat.lean.expected.out
  784. newCatPanic.lean
  785. newCatPanic.lean.expected.out
  786. nonAtomicFieldName.lean
  787. nonAtomicFieldName.lean.expected.out
  788. noncompSection.lean
  789. noncompSection.lean.expected.out
  790. nondepArrow.lean
  791. nondepArrow.lean.expected.out
  792. nonfatalattrs.lean
  793. nonfatalattrs.lean.expected.out
  794. nonReserved.lean
  795. nonReserved.lean.expected.out
  796. noTabs.lean
  797. noTabs.lean.expected.out
  798. notationDelab.lean
  799. notationDelab.lean.expected.out
  800. notationPrecheck.lean
  801. notationPrecheck.lean.expected.out
  802. openExport.lean
  803. openExport.lean.expected.out
  804. openScoped.lean
  805. openScoped.lean.expected.out
  806. or_shortcircuit.lean
  807. or_shortcircuit.lean.expected.out
  808. parserPrio.lean
  809. parserPrio.lean.expected.out
  810. partialIssue.lean
  811. partialIssue.lean.expected.out
  812. partialVariable.lean
  813. partialVariable.lean.expected.out
  814. patvar.lean
  815. patvar.lean.expected.out
  816. phashmap_inst_coherence.lean
  817. phashmap_inst_coherence.lean.expected.out
  818. ppExpr.lean
  819. ppExpr.lean.expected.out
  820. PPInstances.lean
  821. PPInstances.lean.expected.out
  822. ppite.lean
  823. ppite.lean.expected.out
  824. pplevel.lean
  825. pplevel.lean.expected.out
  826. ppMotives.lean
  827. ppMotives.lean.expected.out
  828. ppNotationCode.lean
  829. ppNotationCode.lean.expected.out
  830. ppProofs.lean
  831. ppProofs.lean.expected.out
  832. PPRoundtrip.lean
  833. PPRoundtrip.lean.expected.out
  834. ppSyntax.lean
  835. ppSyntax.lean.expected.out
  836. ppUnicode.lean
  837. ppUnicode.lean.expected.out
  838. precissues.lean
  839. precissues.lean.expected.out
  840. private.lean
  841. private.lean.expected.out
  842. privateFieldCopyIssue.lean
  843. privateFieldCopyIssue.lean.expected.out
  844. Process.lean
  845. Process.lean.expected.out
  846. promise.lean
  847. promise.lean.expected.out
  848. protected.lean
  849. protected.lean.expected.out
  850. protectedAlias.lean
  851. protectedAlias.lean.expected.out
  852. prvCtor.lean
  853. prvCtor.lean.expected.out
  854. prvNameWithMacroScopes.lean
  855. prvNameWithMacroScopes.lean.expected.out
  856. pureCoeIssue.lean
  857. pureCoeIssue.lean.expected.out
  858. rat1.lean
  859. rat1.lean.expected.out
  860. readDir.lean
  861. readDir.lean.expected.out
  862. reduceArity.lean
  863. reduceArity.lean.expected.out
  864. redundantAlt.lean
  865. redundantAlt.lean.expected.out
  866. ref1.lean
  867. ref1.lean.expected.out
  868. refineOccursCheck.lean
  869. refineOccursCheck.lean.expected.out
  870. Reformat.lean
  871. Reformat.lean.expected.out
  872. renameBug.lean
  873. renameBug.lean.expected.out
  874. renameI.lean
  875. renameI.lean.expected.out
  876. repr.lean
  877. repr.lean.expected.out
  878. repr_issue.lean
  879. repr_issue.lean.expected.out
  880. resolveGlobalName.lean
  881. resolveGlobalName.lean.expected.out
  882. revertlet.lean
  883. revertlet.lean.expected.out
  884. rewrite.lean
  885. rewrite.lean.expected.out
  886. rfl_simp_thm.lean
  887. rfl_simp_thm.lean.expected.out
  888. root.lean
  889. root.lean.expected.out
  890. runSTBug.lean
  891. runSTBug.lean.expected.out
  892. runTacticMustCatchExceptions.lean
  893. runTacticMustCatchExceptions.lean.expected.out
  894. rwEqThms.lean
  895. rwEqThms.lean.expected.out
  896. rwWithoutOffsetCnstrs.lean
  897. rwWithoutOffsetCnstrs.lean.expected.out
  898. safeShadowing.lean
  899. safeShadowing.lean.expected.out
  900. sanitizeMacroScopes.lean
  901. sanitizeMacroScopes.lean.expected.out
  902. sanitychecks.lean
  903. sanitychecks.lean.expected.out
  904. scientific.lean
  905. scientific.lean.expected.out
  906. scopedInstanceOutsideNamespace.lean
  907. scopedInstanceOutsideNamespace.lean.expected.out
  908. scopedLocalInsts.lean
  909. scopedLocalInsts.lean.expected.out
  910. scopedMacros.lean
  911. scopedMacros.lean.expected.out
  912. scopedTokens.lean
  913. scopedTokens.lean.expected.out
  914. scopedunifhint.lean
  915. scopedunifhint.lean.expected.out
  916. semicolonOrLinebreak.lean
  917. semicolonOrLinebreak.lean.expected.out
  918. sepByIndentQuot.lean
  919. sepByIndentQuot.lean.expected.out
  920. seqToCodeIssue.lean
  921. seqToCodeIssue.lean.expected.out
  922. shadow.lean
  923. shadow.lean.expected.out
  924. simp_all_duplicateHyps.lean
  925. simp_all_duplicateHyps.lean.expected.out
  926. simp_dsimp.lean
  927. simp_dsimp.lean.expected.out
  928. simp_trace.lean
  929. simp_trace.lean.expected.out
  930. simpArgTypeMismatch.lean
  931. simpArgTypeMismatch.lean.expected.out
  932. simpcfg.lean
  933. simpcfg.lean.expected.out
  934. simpDisch.lean
  935. simpDisch.lean.expected.out
  936. simpPrefixIssue.lean
  937. simpPrefixIssue.lean.expected.out
  938. simpZetaFalse.lean
  939. simpZetaFalse.lean.expected.out
  940. sizeof.lean
  941. sizeof.lean.expected.out
  942. smartUnfolding.lean
  943. smartUnfolding.lean.expected.out
  944. smartUnfoldingMatch.lean
  945. smartUnfoldingMatch.lean.expected.out
  946. sorryAtError.lean
  947. sorryAtError.lean.expected.out
  948. sorryWarning.lean
  949. sorryWarning.lean.expected.out
  950. specializeAttr.lean
  951. specializeAttr.lean.expected.out
  952. splitIssue.lean
  953. splitIssue.lean.expected.out
  954. stdio.lean
  955. stdio.lean.expected.out
  956. stream.lean
  957. stream.lean.expected.out
  958. strictImplicit.lean
  959. strictImplicit.lean.expected.out
  960. string_imp.lean
  961. string_imp.lean.expected.out
  962. string_imp2.lean
  963. string_imp2.lean.expected.out
  964. struct1.lean
  965. struct1.lean.expected.out
  966. structAutoBound.lean
  967. structAutoBound.lean.expected.out
  968. structDefault.lean
  969. structDefault.lean.expected.out
  970. structDefValueOverride.lean
  971. structDefValueOverride.lean.expected.out
  972. structInst1.lean
  973. structInst1.lean.expected.out
  974. structInstError.lean
  975. structInstError.lean.expected.out
  976. structSorryBug.lean
  977. structSorryBug.lean.expected.out
  978. structuralEqns.lean
  979. structuralEqns.lean.expected.out
  980. StxQuot.lean
  981. StxQuot.lean.expected.out
  982. substBadMotive.lean
  983. substBadMotive.lean.expected.out
  984. substlet.lean
  985. substlet.lean.expected.out
  986. syntaxErrors.lean
  987. syntaxErrors.lean.expected.out
  988. syntaxInNamespacesAndPP.lean
  989. syntaxInNamespacesAndPP.lean.expected.out
  990. syntaxPrec.lean
  991. syntaxPrec.lean.expected.out
  992. syntheticHolesAsPatterns.lean
  993. syntheticHolesAsPatterns.lean.expected.out
  994. tabulate.lean
  995. tabulate.lean.expected.out
  996. tacUnsolvedGoalsErrors.lean
  997. tacUnsolvedGoalsErrors.lean.expected.out
  998. tcloop.lean
  999. tcloop.lean.expected.out
  1000. termination_by.lean
  1001. termination_by.lean.expected.out
  1002. termination_by2.lean
  1003. termination_by2.lean.expected.out
  1004. terminationFailure.lean
  1005. terminationFailure.lean.expected.out
  1006. test_single.sh
  1007. theoremType.lean
  1008. theoremType.lean.expected.out
  1009. thunk.lean
  1010. thunk.lean.expected.out
  1011. toFieldNameIssue.lean
  1012. toFieldNameIssue.lean.expected.out
  1013. tokenErrors.lean
  1014. tokenErrors.lean.expected.out
  1015. tooManyVarsAtInduction.lean
  1016. tooManyVarsAtInduction.lean.expected.out
  1017. traceClassScopes.lean
  1018. traceClassScopes.lean.expected.out
  1019. traceStateBactracking.lean
  1020. traceStateBactracking.lean.expected.out
  1021. traceTacticSteps.lean
  1022. traceTacticSteps.lean.expected.out
  1023. treeMap.lean
  1024. treeMap.lean.expected.out
  1025. typeIncorrectPat.lean
  1026. typeIncorrectPat.lean.expected.out
  1027. typeMismatch.lean
  1028. typeMismatch.lean.expected.out
  1029. typeOf.lean
  1030. typeOf.lean.expected.out
  1031. uintCtors.lean
  1032. uintCtors.lean.expected.out
  1033. uintMatch.lean
  1034. uintMatch.lean.expected.out
  1035. unboxStruct.lean
  1036. unboxStruct.lean.expected.out
  1037. unexpander.lean
  1038. unexpander.lean.expected.out
  1039. unexpandersNamespaces.lean
  1040. unexpandersNamespaces.lean.expected.out
  1041. UnexpandSubtype.lean
  1042. UnexpandSubtype.lean.expected.out
  1043. unfold1.lean
  1044. unfold1.lean.expected.out
  1045. unfoldDefEq.lean
  1046. unfoldDefEq.lean.expected.out
  1047. unfoldFailure.lean
  1048. unfoldFailure.lean.expected.out
  1049. unfoldReduceMatch.lean
  1050. unfoldReduceMatch.lean.expected.out
  1051. unhygienic.lean
  1052. unhygienic.lean.expected.out
  1053. unhygienicCode.lean
  1054. unhygienicCode.lean.expected.out
  1055. unifHintAndTC.lean
  1056. unifHintAndTC.lean.expected.out
  1057. univInference.lean
  1058. univInference.lean.expected.out
  1059. unknownId.lean
  1060. unknownId.lean.expected.out
  1061. unknownTactic.lean
  1062. unknownTactic.lean.expected.out
  1063. unnecessaryUnfolding.lean
  1064. unnecessaryUnfolding.lean.expected.out
  1065. unsolvedIndCases.lean
  1066. unsolvedIndCases.lean.expected.out
  1067. unsound.lean
  1068. unsound.lean.expected.out
  1069. unused_univ.lean
  1070. unused_univ.lean.expected.out
  1071. unusedLet.lean
  1072. unusedLet.lean.expected.out
  1073. unusedWarningAtStructUpdate.lean
  1074. unusedWarningAtStructUpdate.lean.expected.out
  1075. updateExprIssue.lean
  1076. updateExprIssue.lean.expected.out
  1077. updateLevelIssues.lean
  1078. updateLevelIssues.lean.expected.out
  1079. Uri.lean
  1080. Uri.lean.expected.out
  1081. varBinderUpdate.lean
  1082. varBinderUpdate.lean.expected.out
  1083. warningAsError.lean
  1084. warningAsError.lean.expected.out
  1085. wf1.lean
  1086. wf1.lean.expected.out
  1087. wf2.lean
  1088. wf2.lean.expected.out
  1089. wfrecUnusedLet.lean
  1090. wfrecUnusedLet.lean.expected.out
  1091. whnfProj.lean
  1092. whnfProj.lean.expected.out
  1093. wildcardAlt.lean
  1094. wildcardAlt.lean.expected.out
  1095. withAssignableSyntheticOpaqueBug.lean
  1096. withAssignableSyntheticOpaqueBug.lean.expected.out
  1097. workspaceSymbols.lean
  1098. workspaceSymbols.lean.expected.out
  1099. zipper.lean
  1100. zipper.lean.expected.out