提示

对于游戏开发来说，最重要的可能是"提示"。您可以使用 Hint 策略在证明的任何地方添加提示

Statement .... := by
  Hint "开始时显示的提示"
  rw [h]
  Hint "使用 rw 后的一些提示"
  ...

注意提示只是上下文感知但不是历史感知。特别是，它们只查看假设和当前目标。如果玩家决定采用独特的证明思路，他们可能会以不同的顺序遇到提示 - 或者根本不会遇到。Branch 策略有助于在示例解决方案的证明之外放置提示。

1. 提示何时显示？

如果玩家的目标与示例解决方案中放置提示的目标匹配，并且示例解决方案的整个上下文都存在于玩家的上下文中，则会显示提示。玩家的上下文可能包含额外的证明。

这意味着如果您有多个相同的子目标，您应该只在其中一个中放置单个提示，它将在所有子目标中显示。

但是，在前一步中已经存在的相同（非隐藏）提示会被省略。这是为了允许玩家给证明添加新假设，例如使用 have，而不会一遍又一遍地看到相同的提示。隐藏提示不会被过滤。

您可以使用 Branch 在死胡同或替代证明分支中放置提示。

Branch 块内的证明通常由 lean 评估，但在最后被丢弃，因此在证明目标方面没有取得进展。

Statement .... := by
  Hint "使用 `rw` 或 `rewrite`。"
  Branch
    rewrite [h]
    Hint "现在您仍然需要 `rfl`"
  rw [h]

将提示文本中的变量放在括号内，如：{h}！这样服务器可以将变量名替换为用户实际使用的名称。

注意：这意味着您需要转义任何其他开放大括号的使用（即 \{）。另请参见游戏中的 LaTeX 的示例。

例如，如果示例证明包含

have h : True := trivial
Hint "现在使用 `rw [{h}]` 来使用您的假设 `{h}`。"

但玩家写 have g : True := trivial，他们将看到提示说 "现在使用 rw [g] 来使用您的假设 g。"

一些提示可以被隐藏，只有在用户点击按钮获取额外帮助后才显示。您用 (hidden := true) 标记提示为隐藏：

Hint (hidden := true) "一些隐藏提示"

如果您使用属性 (strict := true)，只有当整个上下文与放置提示的位置完全匹配时才显示提示。使用 (hint := false)（这是默认值），玩家上下文中是否存在额外假设并不重要。

Hint (strict := true) "现在使用 `have` 创建新假设。"

如果您想给出关于像 have 这样的策略的细粒度详细信息，您可能应该使用 (strict := true)，这些策略不修改目标或任何现有假设，只创建新假设。

您可以使用 Markdown 格式化您的提示，也可以使用 LaTeX。有关更多详细信息，请参见游戏中的 LaTeX。

提示和介绍/结论也可以包含图像。

对于远程图像，只需添加：

<img src=\"https://url.com/to/image\"/>

参见 https://www.jmilne.org/not/Mamscd.pdf

提示和介绍/结论也可以包含图像。

对于远程图像，只需添加：

<img src=\"https://url.com/to/image\"/>

本地图像目前只能通过一个方法包含：

游戏 images/ 文件夹中的图像将在 data/g/[user]/[repo]/[image].[png|jpg|…] 处可访问，因此可以像外部图像一样包含它们。