Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/doc-setup/./tests/lean
tree: 9e58d0f23d0180e62a559e7e3e999e1b66df88c5 [search]
  1. Reformat/
  2. run/
  3. server/
  4. trust0/
  5. .gitignore
  6. 217.lean
  7. 217.lean.expected.out
  8. 220.lean
  9. 220.lean.expected.out
  10. 223.lean
  11. 223.lean.expected.out
  12. 236.lean
  13. 236.lean.expected.out
  14. abst.lean
  15. abst.lean.expected.out
  16. appParserIssue.lean
  17. appParserIssue.lean.expected.out
  18. attrCmd.lean
  19. attrCmd.lean.expected.out
  20. autoBoundImplicits1.lean
  21. autoBoundImplicits1.lean.expected.out
  22. autoBoundImplicits2.lean
  23. autoBoundImplicits2.lean.expected.out
  24. autoPPExplicit.lean
  25. autoPPExplicit.lean.expected.out
  26. auxDeclIssue.lean
  27. auxDeclIssue.lean.expected.out
  28. beginEndAsMacro.lean
  29. beginEndAsMacro.lean.expected.out
  30. binsearch.lean
  31. binsearch.lean.expected.out
  32. bytearray.lean
  33. bytearray.lean.expected.out
  34. cdotTuple.lean
  35. cdotTuple.lean.expected.out
  36. class_def_must_fail.lean
  37. class_def_must_fail.lean.expected.out
  38. classBadOutParam.lean
  39. classBadOutParam.lean.expected.out
  40. collectDepsIssue.lean
  41. collectDepsIssue.lean.expected.out
  42. ctor_layout.lean
  43. ctor_layout.lean.expected.out
  44. dbgMacros.lean
  45. dbgMacros.lean.expected.out
  46. decimals.lean
  47. decimals.lean.expected.out
  48. defaultInstance.lean
  49. defaultInstance.lean.expected.out
  50. derivingRepr.lean
  51. derivingRepr.lean.expected.out
  52. doIfLet.lean
  53. doIfLet.lean.expected.out
  54. doIssue.lean
  55. doIssue.lean.expected.out
  56. doNotation1.lean
  57. doNotation1.lean.expected.out
  58. doSeqRightIssue.lean
  59. doSeqRightIssue.lean.expected.out
  60. elseifDoErrorPos.lean
  61. elseifDoErrorPos.lean.expected.out
  62. emptyc.lean
  63. emptyc.lean.expected.out
  64. envExtensionSealed.lean
  65. envExtensionSealed.lean.expected.out
  66. eval_except.lean
  67. eval_except.lean.expected.out
  68. evalWithMVar.lean
  69. evalWithMVar.lean.expected.out
  70. exitAfterParseError.lean
  71. exitAfterParseError.lean.expected.out
  72. extract.lean
  73. extract.lean.expected.out
  74. file_not_found.lean
  75. file_not_found.lean.expected.out
  76. forErrors.lean
  77. forErrors.lean.expected.out
  78. Format.lean
  79. Format.lean.expected.out
  80. funExpected.lean
  81. funExpected.lean.expected.out
  82. hidingInaccessibleNames.lean
  83. hidingInaccessibleNames.lean.expected.out
  84. holeErrors.lean
  85. holeErrors.lean.expected.out
  86. holes.lean
  87. holes.lean.expected.out
  88. hygienicIntro.lean
  89. hygienicIntro.lean.expected.out
  90. inductionErrors.lean
  91. inductionErrors.lean.expected.out
  92. inductive1.lean
  93. inductive1.lean.expected.out
  94. infoFromFailure.lean
  95. infoFromFailure.lean.expected.out
  96. inst.lean
  97. inst.lean.expected.out
  98. invalidFieldName.lean
  99. invalidFieldName.lean.expected.out
  100. invalidNamedArgs.lean
  101. invalidNamedArgs.lean.expected.out
  102. IRbug.lean
  103. IRbug.lean.expected.out
  104. json.lean
  105. json.lean.expected.out
  106. letrec1.lean
  107. letrec1.lean.expected.out
  108. letrecErrors.lean
  109. letrecErrors.lean.expected.out
  110. ll_infer_type_bug.lean
  111. ll_infer_type_bug.lean.expected.out
  112. lvl1.lean
  113. lvl1.lean.expected.out
  114. macroPrio.lean
  115. macroPrio.lean.expected.out
  116. macroscopes.lean
  117. macroscopes.lean.expected.out
  118. macroStack.lean
  119. macroStack.lean.expected.out
  120. match1.lean
  121. match1.lean.expected.out
  122. match2.lean
  123. match2.lean.expected.out
  124. match3.lean
  125. match3.lean.expected.out
  126. match4.lean
  127. match4.lean.expected.out
  128. matchErrorLocation.lean
  129. matchErrorLocation.lean.expected.out
  130. missingExplicitWithForwardNamedDep.lean
  131. missingExplicitWithForwardNamedDep.lean.expected.out
  132. mutualdef1.lean
  133. mutualdef1.lean.expected.out
  134. mutualWithNamespaceMacro.lean
  135. mutualWithNamespaceMacro.lean.expected.out
  136. mvar1.lean
  137. mvar1.lean.expected.out
  138. mvar2.lean
  139. mvar2.lean.expected.out
  140. mvar3.lean
  141. mvar3.lean.expected.out
  142. mvar_fvar.lean
  143. mvar_fvar.lean.expected.out
  144. namedHoles.lean
  145. namedHoles.lean.expected.out
  146. namelit.lean
  147. namelit.lean.expected.out
  148. nonReserved.lean
  149. nonReserved.lean.expected.out
  150. openExport.lean
  151. openExport.lean.expected.out
  152. or_shortcircuit.lean
  153. or_shortcircuit.lean.expected.out
  154. parserPrio.lean
  155. parserPrio.lean.expected.out
  156. phashmap_inst_coherence.lean
  157. phashmap_inst_coherence.lean.expected.out
  158. ppExpr.lean
  159. ppExpr.lean.expected.out
  160. ppite.lean
  161. ppite.lean.expected.out
  162. pplevel.lean
  163. pplevel.lean.expected.out
  164. PPRoundtrip.lean
  165. PPRoundtrip.lean.expected.out
  166. ppSyntax.lean
  167. ppSyntax.lean.expected.out
  168. precissues.lean
  169. precissues.lean.expected.out
  170. private.lean
  171. private.lean.expected.out
  172. Process.lean
  173. Process.lean.expected.out
  174. protected.lean
  175. protected.lean.expected.out
  176. pureCoeIssue.lean
  177. pureCoeIssue.lean.expected.out
  178. readlinkf.sh
  179. redundantAlt.lean
  180. redundantAlt.lean.expected.out
  181. ref1.lean
  182. ref1.lean.expected.out
  183. Reformat.lean
  184. Reformat.lean.expected.out
  185. repr.lean
  186. repr.lean.expected.out
  187. repr_issue.lean
  188. repr_issue.lean.expected.out
  189. resolveGlobalName.lean
  190. resolveGlobalName.lean.expected.out
  191. revertlet.lean
  192. revertlet.lean.expected.out
  193. rewrite.lean
  194. rewrite.lean.expected.out
  195. runSTBug.lean
  196. runSTBug.lean.expected.out
  197. sanitizeMacroScopes.lean
  198. sanitizeMacroScopes.lean.expected.out
  199. sanitychecks.lean
  200. sanitychecks.lean.expected.out
  201. scopedInstanceOutsideNamespace.lean
  202. scopedInstanceOutsideNamespace.lean.expected.out
  203. scopedLocalInsts.lean
  204. scopedLocalInsts.lean.expected.out
  205. scopedMacros.lean
  206. scopedMacros.lean.expected.out
  207. scopedTokens.lean
  208. scopedTokens.lean.expected.out
  209. scopedunifhint.lean
  210. scopedunifhint.lean.expected.out
  211. shadow.lean
  212. shadow.lean.expected.out
  213. simpcfg.lean
  214. simpcfg.lean.expected.out
  215. smartUnfolding.lean
  216. smartUnfolding.lean.expected.out
  217. stdio.lean
  218. stdio.lean.expected.out
  219. stream.lean
  220. stream.lean.expected.out
  221. string_imp.lean
  222. string_imp.lean.expected.out
  223. string_imp2.lean
  224. string_imp2.lean.expected.out
  225. struct1.lean
  226. struct1.lean.expected.out
  227. structAutoBound.lean
  228. structAutoBound.lean.expected.out
  229. structDefault.lean
  230. structDefault.lean.expected.out
  231. structInstError.lean
  232. structInstError.lean.expected.out
  233. StxQuot.lean
  234. StxQuot.lean.expected.out
  235. substlet.lean
  236. substlet.lean.expected.out
  237. syntaxErrors.lean
  238. syntaxErrors.lean.expected.out
  239. syntaxInNamespacesAndPP.lean
  240. syntaxInNamespacesAndPP.lean.expected.out
  241. test_single.sh
  242. typeIncorrectPat.lean
  243. typeIncorrectPat.lean.expected.out
  244. typeMismatch.lean
  245. typeMismatch.lean.expected.out
  246. typeOf.lean
  247. typeOf.lean.expected.out
  248. uintCtors.lean
  249. uintCtors.lean.expected.out
  250. univInference.lean
  251. univInference.lean.expected.out
  252. unknownId.lean
  253. unknownId.lean.expected.out
  254. unknownTactic.lean
  255. unknownTactic.lean.expected.out
  256. unnecessaryUnfolding.lean
  257. unnecessaryUnfolding.lean.expected.out
  258. unsolvedIndCases.lean
  259. unsolvedIndCases.lean.expected.out
  260. unused_univ.lean
  261. unused_univ.lean.expected.out
  262. weirdmacro.lean
  263. weirdmacro.lean.expected.out
  264. zipper.lean
  265. zipper.lean.expected.out