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