kframework - # 关键字的文档，例如 #as?

Question

是否有关于#as可用关键字以及如何使用它们的文档？

特别是#as意味着<k> S:Set </k> #as ASET是ASETSet 还是等于k其中包含的单元格S？

语法<k> ... SetItem(X) ... #as S </k>有效吗？

Answer 1

这是#as模式的文档：https ://github.com/kframework/k/blob/master/pending-documentation.md#as-patterns

在您的第一个示例中：

<k> S:Set </k> #as KCELL

将变量绑定S到单元格包含的实际值Set，<k>并将绑定KCELL到整个<k>-cell term <k> S:Set </k>。

在您的第二个示例（修改）中：

<k> (REST SetItem(X)) #as S </k>

您将被X绑定到被挑选出来的元素（没有任何限制，它将不确定地挑选），REST绑定到没有该元素的集合的其余部分，并S绑定到整个集合。