问证明卷曲大括号的语法:开始x. ={auto} y. []
EN

Stack Overflow用户

提问于 2022-02-26 14:51:21

回答 1查看 55关注 0票数 0

我看到了Coq证明中使用的以下语法，以及关系(=)和策略(auto)的变体：

begin
  x.
= { auto }
  y.
= { auto }
  z.
[].

这个句法结构的名称是什么，在哪里有文档记录？

回答已采纳

发布于 2022-02-26 17:37:43

这似乎是你所链接的项目定义的一种战术符号。这是定义符号的文件，从第84行开始。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/71277610

复制

相似问题

问证明卷曲大括号的语法:开始x. ={auto} y. []EN