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