syntax - Coq 介绍语法

Question

有人可以解释一下下面的 intros 语法吗？

Lemma is_single_nBTP : forall t, is_single_nBT t = true -> exists n : nat, t = Leaf n.
Proof.
intros [ nleaf | nnode t1 t2] h.
exists nleaf.
reflexivity.
...

其中nBT是nat二叉树，is_single_nBT是一个函数，当t为true时返回true一片叶子。

(这个例子来自这个lecture。)

Answer 1

[A | B] 是一个析取模式。这与函数式编程语言中的案例分析是相同的思想。

在这种情况下，您要创建两个子目标。一个已知 t 是一个以自然数 nleaf 作为参数的叶子，另一个是 t 作为 引入的带有参数 nnode、t1 和 t2 的节点。

另一种说法 h : is_single_nBT ? = true 被引入，其中 ? 是 Leaf nleaf 或 Node nnode t1 t2。