Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/elab-command-rec/./tests/lean
tree: d168ac88fa33f573fb5a5308354743c04ee81575 [search]
  1. interactive/
  2. Reformat/
  3. run/
  4. server/
  5. trust0/
  6. .gitignore
  7. 217.lean
  8. 217.lean.expected.out
  9. 220.lean
  10. 220.lean.expected.out
  11. 223.lean
  12. 223.lean.expected.out
  13. 236.lean
  14. 236.lean.expected.out
  15. 241.lean
  16. 241.lean.expected.out
  17. 243.lean
  18. 243.lean.expected.out
  19. 247.lean
  20. 247.lean.expected.out
  21. 248.lean
  22. 248.lean.expected.out
  23. 255.lean
  24. 255.lean.expected.out
  25. 276.lean
  26. 276.lean.expected.out
  27. 277a.lean
  28. 277a.lean.expected.out
  29. 277b.lean
  30. 277b.lean.expected.out
  31. 283.lean
  32. 283.lean.expected.out
  33. 297.lean
  34. 297.lean.expected.out
  35. 301.lean
  36. 301.lean.expected.out
  37. 302.lean
  38. 302.lean.expected.out
  39. 307.lean
  40. 307.lean.expected.out
  41. 309.lean
  42. 309.lean.expected.out
  43. 331.lean
  44. 331.lean.expected.out
  45. 343.lean
  46. 343.lean.expected.out
  47. 345.lean
  48. 345.lean.expected.out
  49. 346.lean
  50. 346.lean.expected.out
  51. 348.lean
  52. 348.lean.expected.out
  53. 353.lean
  54. 353.lean.expected.out
  55. 366.lean
  56. 366.lean.expected.out
  57. 386.lean
  58. 386.lean.expected.out
  59. 389.lean
  60. 389.lean.expected.out
  61. 414.lean
  62. 414.lean.expected.out
  63. 415.lean
  64. 415.lean.expected.out
  65. 421.lean
  66. 421.lean.expected.out
  67. 423.lean
  68. 423.lean.expected.out
  69. 435.lean
  70. 435.lean.expected.out
  71. 435b.lean
  72. 435b.lean.expected.out
  73. 439.lean
  74. 439.lean.expected.out
  75. 440.lean
  76. 440.lean.expected.out
  77. 448.lean
  78. 448.lean.expected.out
  79. 449.lean
  80. 449.lean.expected.out
  81. 450.lean
  82. 450.lean.expected.out
  83. 456.lean
  84. 456.lean.expected.out
  85. 496.lean
  86. 496.lean.expected.out
  87. abst.lean
  88. abst.lean.expected.out
  89. appParserIssue.lean
  90. appParserIssue.lean.expected.out
  91. attrCmd.lean
  92. attrCmd.lean.expected.out
  93. autobound_and_macroscopes.lean
  94. autobound_and_macroscopes.lean.expected.out
  95. autoBoundErrorMsg.lean
  96. autoBoundErrorMsg.lean.expected.out
  97. autoBoundImplicits1.lean
  98. autoBoundImplicits1.lean.expected.out
  99. autoBoundImplicits2.lean
  100. autoBoundImplicits2.lean.expected.out
  101. autoBoundPostponeLoop.lean
  102. autoBoundPostponeLoop.lean.expected.out
  103. autoPPExplicit.lean
  104. autoPPExplicit.lean.expected.out
  105. auxDeclIssue.lean
  106. auxDeclIssue.lean.expected.out
  107. badBinderName.lean
  108. badBinderName.lean.expected.out
  109. badIhName.lean
  110. badIhName.lean.expected.out
  111. beginEndAsMacro.lean
  112. beginEndAsMacro.lean.expected.out
  113. bigUnivOffsets.lean
  114. bigUnivOffsets.lean.expected.out
  115. binderCacheIssue.lean
  116. binderCacheIssue.lean.expected.out
  117. binderCacheIssue2.lean
  118. binderCacheIssue2.lean.expected.out
  119. binsearch.lean
  120. binsearch.lean.expected.out
  121. bitwise.lean
  122. bitwise.lean.expected.out
  123. bytearray.lean
  124. bytearray.lean.expected.out
  125. cacheIssue.lean
  126. cacheIssue.lean.expected.out
  127. cdotAtSimpArg.lean
  128. cdotAtSimpArg.lean.expected.out
  129. cdotTuple.lean
  130. cdotTuple.lean.expected.out
  131. class_def_must_fail.lean
  132. class_def_must_fail.lean.expected.out
  133. classBadOutParam.lean
  134. classBadOutParam.lean.expected.out
  135. collectDepsIssue.lean
  136. collectDepsIssue.lean.expected.out
  137. commandPrefix.lean
  138. commandPrefix.lean.expected.out
  139. constDelab.lean
  140. constDelab.lean.expected.out
  141. constructorTac.lean
  142. constructorTac.lean.expected.out
  143. copy-produced
  144. ctor_layout.lean
  145. ctor_layout.lean.expected.out
  146. dbgMacros.lean
  147. dbgMacros.lean.expected.out
  148. decimals.lean
  149. decimals.lean.expected.out
  150. defaultInstance.lean
  151. defaultInstance.lean.expected.out
  152. delabUnexpand.lean
  153. delabUnexpand.lean.expected.out
  154. derivingRepr.lean
  155. derivingRepr.lean.expected.out
  156. docStr.lean
  157. docStr.lean.expected.out
  158. doErrorMsg.lean
  159. doErrorMsg.lean.expected.out
  160. doIfLet.lean
  161. doIfLet.lean.expected.out
  162. doIssue.lean
  163. doIssue.lean.expected.out
  164. doLetLoop.lean
  165. doLetLoop.lean.expected.out
  166. doNotation1.lean
  167. doNotation1.lean.expected.out
  168. doSeqRightIssue.lean
  169. doSeqRightIssue.lean.expected.out
  170. eagerCoeExpansion.lean
  171. eagerCoeExpansion.lean.expected.out
  172. eagerUnfoldingIssue.lean
  173. eagerUnfoldingIssue.lean.expected.out
  174. elseifDoErrorPos.lean
  175. elseifDoErrorPos.lean.expected.out
  176. emptyc.lean
  177. emptyc.lean.expected.out
  178. eoi.lean
  179. eoi.lean.expected.out
  180. eraseSimp.lean
  181. eraseSimp.lean.expected.out
  182. errorRecoveryBug.lean
  183. errorRecoveryBug.lean.expected.out
  184. eta.lean
  185. eta.lean.expected.out
  186. eval_except.lean
  187. eval_except.lean.expected.out
  188. evalSorry.lean
  189. evalSorry.lean.expected.out
  190. evalWithMVar.lean
  191. evalWithMVar.lean.expected.out
  192. exactErrorPos.lean
  193. exactErrorPos.lean.expected.out
  194. exitAfterParseError.lean
  195. exitAfterParseError.lean.expected.out
  196. extract.lean
  197. extract.lean.expected.out
  198. file_not_found.lean
  199. file_not_found.lean.expected.out
  200. filePath.lean
  201. filePath.lean.expected.out
  202. forErrors.lean
  203. forErrors.lean.expected.out
  204. Format.lean
  205. Format.lean.expected.out
  206. funExpected.lean
  207. funExpected.lean.expected.out
  208. funInfoBug.lean
  209. funInfoBug.lean.expected.out
  210. gcd.lean
  211. gcd.lean.expected.out
  212. have.lean
  213. have.lean.expected.out
  214. hidingInaccessibleNames.lean
  215. hidingInaccessibleNames.lean.expected.out
  216. holeErrors.lean
  217. holeErrors.lean.expected.out
  218. holes.lean
  219. holes.lean.expected.out
  220. hygienicIntro.lean
  221. hygienicIntro.lean.expected.out
  222. implicitLambdaIssue.lean
  223. implicitLambdaIssue.lean.expected.out
  224. inductionErrors.lean
  225. inductionErrors.lean.expected.out
  226. inductionGen.lean
  227. inductionGen.lean.expected.out
  228. inductive1.lean
  229. inductive1.lean.expected.out
  230. infoFromFailure.lean
  231. infoFromFailure.lean.expected.out
  232. infoTree.lean
  233. infoTree.lean.expected.out
  234. inst.lean
  235. inst.lean.expected.out
  236. intModBug.lean
  237. intModBug.lean.expected.out
  238. intNegSucc.lean
  239. intNegSucc.lean.expected.out
  240. invalidFieldName.lean
  241. invalidFieldName.lean.expected.out
  242. invalidInstImplicit.lean
  243. invalidInstImplicit.lean.expected.out
  244. invalidNamedArgs.lean
  245. invalidNamedArgs.lean.expected.out
  246. IRbug.lean
  247. IRbug.lean.expected.out
  248. isDefEqOffsetBug.lean
  249. isDefEqOffsetBug.lean.expected.out
  250. jason1.lean
  251. jason1.lean.expected.out
  252. jason2.lean
  253. jason2.lean.expected.out
  254. json.lean
  255. json.lean.expected.out
  256. letrec1.lean
  257. letrec1.lean.expected.out
  258. letrecErrors.lean
  259. letrecErrors.lean.expected.out
  260. liftOverLeft.lean
  261. liftOverLeft.lean.expected.out
  262. ll_infer_type_bug.lean
  263. ll_infer_type_bug.lean.expected.out
  264. localNotationPP.lean
  265. localNotationPP.lean.expected.out
  266. loopErrorRecovery.lean
  267. loopErrorRecovery.lean.expected.out
  268. lvl1.lean
  269. lvl1.lean.expected.out
  270. macroPrio.lean
  271. macroPrio.lean.expected.out
  272. macroResolveName.lean
  273. macroResolveName.lean.expected.out
  274. macroscopes.lean
  275. macroscopes.lean.expected.out
  276. macroStack.lean
  277. macroStack.lean.expected.out
  278. macroTrace.lean
  279. macroTrace.lean.expected.out
  280. mangling.lean
  281. mangling.lean.expected.out
  282. match1.lean
  283. match1.lean.expected.out
  284. match2.lean
  285. match2.lean.expected.out
  286. match3.lean
  287. match3.lean.expected.out
  288. match4.lean
  289. match4.lean.expected.out
  290. matchAltIndent.lean
  291. matchAltIndent.lean.expected.out
  292. matchApp.lean
  293. matchApp.lean.expected.out
  294. matchErrorLocation.lean
  295. matchErrorLocation.lean.expected.out
  296. matchErrorMsg.lean
  297. matchErrorMsg.lean.expected.out
  298. matchMissingCasesAsStuckError.lean
  299. matchMissingCasesAsStuckError.lean.expected.out
  300. matchunit.lean
  301. matchunit.lean.expected.out
  302. matchUnknownFVarBug.lean
  303. matchUnknownFVarBug.lean.expected.out
  304. missingExplicitWithForwardNamedDep.lean
  305. missingExplicitWithForwardNamedDep.lean.expected.out
  306. modBug.lean
  307. modBug.lean.expected.out
  308. moduleOf.lean
  309. moduleOf.lean.expected.out
  310. mulcommErrorMessage.lean
  311. mulcommErrorMessage.lean.expected.out
  312. mutualdef1.lean
  313. mutualdef1.lean.expected.out
  314. mutualWithNamespaceMacro.lean
  315. mutualWithNamespaceMacro.lean.expected.out
  316. mvar1.lean
  317. mvar1.lean.expected.out
  318. mvar2.lean
  319. mvar2.lean.expected.out
  320. mvar3.lean
  321. mvar3.lean.expected.out
  322. mvar_fvar.lean
  323. mvar_fvar.lean.expected.out
  324. mvarAtDefaultValue.lean
  325. mvarAtDefaultValue.lean.expected.out
  326. namedHoles.lean
  327. namedHoles.lean.expected.out
  328. namelit.lean
  329. namelit.lean.expected.out
  330. negFloat.lean
  331. negFloat.lean.expected.out
  332. newCatPanic.lean
  333. newCatPanic.lean.expected.out
  334. nonReserved.lean
  335. nonReserved.lean.expected.out
  336. noTabs.lean
  337. noTabs.lean.expected.out
  338. notationPrecheck.lean
  339. notationPrecheck.lean.expected.out
  340. openExport.lean
  341. openExport.lean.expected.out
  342. or_shortcircuit.lean
  343. or_shortcircuit.lean.expected.out
  344. parserPrio.lean
  345. parserPrio.lean.expected.out
  346. partialVariable.lean
  347. partialVariable.lean.expected.out
  348. patvar.lean
  349. patvar.lean.expected.out
  350. phashmap_inst_coherence.lean
  351. phashmap_inst_coherence.lean.expected.out
  352. ppExpr.lean
  353. ppExpr.lean.expected.out
  354. ppite.lean
  355. ppite.lean.expected.out
  356. pplevel.lean
  357. pplevel.lean.expected.out
  358. ppMotives.lean
  359. ppMotives.lean.expected.out
  360. ppNotationCode.lean
  361. ppNotationCode.lean.expected.out
  362. ppProofs.lean
  363. ppProofs.lean.expected.out
  364. PPRoundtrip.lean
  365. PPRoundtrip.lean.expected.out
  366. ppSyntax.lean
  367. ppSyntax.lean.expected.out
  368. precissues.lean
  369. precissues.lean.expected.out
  370. private.lean
  371. private.lean.expected.out
  372. Process.lean
  373. Process.lean.expected.out
  374. protected.lean
  375. protected.lean.expected.out
  376. pureCoeIssue.lean
  377. pureCoeIssue.lean.expected.out
  378. readDir.lean
  379. readDir.lean.expected.out
  380. readlinkf.sh
  381. redundantAlt.lean
  382. redundantAlt.lean.expected.out
  383. ref1.lean
  384. ref1.lean.expected.out
  385. Reformat.lean
  386. Reformat.lean.expected.out
  387. repr.lean
  388. repr.lean.expected.out
  389. repr_issue.lean
  390. repr_issue.lean.expected.out
  391. resolveGlobalName.lean
  392. resolveGlobalName.lean.expected.out
  393. revertlet.lean
  394. revertlet.lean.expected.out
  395. rewrite.lean
  396. rewrite.lean.expected.out
  397. runSTBug.lean
  398. runSTBug.lean.expected.out
  399. safeShadowing.lean
  400. safeShadowing.lean.expected.out
  401. sanitizeMacroScopes.lean
  402. sanitizeMacroScopes.lean.expected.out
  403. sanitychecks.lean
  404. sanitychecks.lean.expected.out
  405. scopedInstanceOutsideNamespace.lean
  406. scopedInstanceOutsideNamespace.lean.expected.out
  407. scopedLocalInsts.lean
  408. scopedLocalInsts.lean.expected.out
  409. scopedMacros.lean
  410. scopedMacros.lean.expected.out
  411. scopedTokens.lean
  412. scopedTokens.lean.expected.out
  413. scopedunifhint.lean
  414. scopedunifhint.lean.expected.out
  415. shadow.lean
  416. shadow.lean.expected.out
  417. simpArgTypeMismatch.lean
  418. simpArgTypeMismatch.lean.expected.out
  419. simpcfg.lean
  420. simpcfg.lean.expected.out
  421. sizeof.lean
  422. sizeof.lean.expected.out
  423. smartUnfolding.lean
  424. smartUnfolding.lean.expected.out
  425. sorryAtError.lean
  426. sorryAtError.lean.expected.out
  427. sorryWarning.lean
  428. sorryWarning.lean.expected.out
  429. stdio.lean
  430. stdio.lean.expected.out
  431. stream.lean
  432. stream.lean.expected.out
  433. string_imp.lean
  434. string_imp.lean.expected.out
  435. string_imp2.lean
  436. string_imp2.lean.expected.out
  437. struct1.lean
  438. struct1.lean.expected.out
  439. structAutoBound.lean
  440. structAutoBound.lean.expected.out
  441. structDefault.lean
  442. structDefault.lean.expected.out
  443. structInstError.lean
  444. structInstError.lean.expected.out
  445. structSorryBug.lean
  446. structSorryBug.lean.expected.out
  447. StxQuot.lean
  448. StxQuot.lean.expected.out
  449. substlet.lean
  450. substlet.lean.expected.out
  451. syntaxErrors.lean
  452. syntaxErrors.lean.expected.out
  453. syntaxInNamespacesAndPP.lean
  454. syntaxInNamespacesAndPP.lean.expected.out
  455. tacUnsolvedGoalsErrors.lean
  456. tacUnsolvedGoalsErrors.lean.expected.out
  457. tcloop.lean
  458. tcloop.lean.expected.out
  459. test_single.sh
  460. theoremType.lean
  461. theoremType.lean.expected.out
  462. thunk.lean
  463. thunk.lean.expected.out
  464. tokenErrors.lean
  465. tokenErrors.lean.expected.out
  466. tooManyVarsAtInduction.lean
  467. tooManyVarsAtInduction.lean.expected.out
  468. typeIncorrectPat.lean
  469. typeIncorrectPat.lean.expected.out
  470. typeMismatch.lean
  471. typeMismatch.lean.expected.out
  472. typeOf.lean
  473. typeOf.lean.expected.out
  474. uintCtors.lean
  475. uintCtors.lean.expected.out
  476. unhygienic.lean
  477. unhygienic.lean.expected.out
  478. unifHintAndTC.lean
  479. unifHintAndTC.lean.expected.out
  480. univInference.lean
  481. univInference.lean.expected.out
  482. unknownId.lean
  483. unknownId.lean.expected.out
  484. unknownTactic.lean
  485. unknownTactic.lean.expected.out
  486. unnecessaryUnfolding.lean
  487. unnecessaryUnfolding.lean.expected.out
  488. unsolvedIndCases.lean
  489. unsolvedIndCases.lean.expected.out
  490. unused_univ.lean
  491. unused_univ.lean.expected.out
  492. weirdmacro.lean
  493. weirdmacro.lean.expected.out
  494. whnfProj.lean
  495. whnfProj.lean.expected.out
  496. zipper.lean
  497. zipper.lean.expected.out