13.9. 空洞🔗

空洞或占位项是一种表示没有向精译器提供指令的项。在项中，如果周围上下文只允许在空洞处写下一个类型正确的项，空洞就可以自动填充。否则，空洞会导致错误。在模式中，空洞表示可以匹配任何值的全匹配模式。

语法空洞

空洞用下划线书写。

term ::= ...
    | _

通过合一填充空洞

函数 the 的用法类似于 Lean.Parser.Term.show : termshow 或类型标注。

def the (α : Sort u) (x : α) : α := x

如果可以推断第二个参数的类型，那么第一个参数可以是空洞。以下两个命令等价：

the String "Hello!" : String#check the String "Hello!"

the String "Hello" : String#check the _ "Hello"

在线查看 ↪

编写证明时，显式引入未知值可能很方便。这通过合成空洞实现；合成空洞永远不会通过合一求解，并且可以出现在多个位置。它们主要用于策略证明，详见证明中的元变量一节。

语法合成空洞

term ::= ...
    | ?ident

term ::= ...
    | ?_