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