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