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